mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.toWeightBasis.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : P.IsRootSystem], b.toWeightBasis = b.toWeightBasis
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.prod_dirac : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  [MeasureTheory.SFinite μ] (y : β),
  μ.prod (MeasureTheory.Measure.dirac y) = MeasureTheory.Measure.map (fun x => (x, y)) μ
-- Mathlib.Logic.Equiv.Defs
Equiv.apply_symm_apply : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β) (x : β), e (e.symm x) = x
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
/-- An extension of the `ContinuousFunctionalCalculus` requiring that `cfcHom` is an isometry.  -/
IsometricContinuousFunctionalCalculus : (R : Type u_1) →
  (A : Type u_2) →
    outParam (A → Prop) →
      [inst : CommSemiring R] →
        [inst_1 : StarRing R] →
          [inst_2 : MetricSpace R] →
            [IsTopologicalSemiring R] →
              [ContinuousStar R] → [inst_5 : Ring A] → [StarRing A] → [MetricSpace A] → [Algebra R A] → Prop
-- Init.Data.Int.Compare
Int.compare_ne_gt : ∀ {a b : ℤ}, compare a b ≠ Ordering.gt ↔ a ≤ b
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffAt.sum : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {x₀ : M} {t : Finset ι} {f : ι → M → G},
  (∀ i ∈ t, ContMDiffAt I' I n (f i) x₀) → ContMDiffAt I' I n (fun x => ∑ i ∈ t, f i x) x₀
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.le_ofSlice_iff : ∀ {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos},
  q ≤ String.Slice.Pos.ofSlice p ↔ ∃ (h₁ : q ≤ p₁), ∀ (h₀ : p₀ ≤ q), q.slice p₀ p₁ h₀ h₁ ≤ p
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
riemannZeta₁.eq_1 : ∀ (s : ℂ), riemannZeta₁ s = 1 + (s - 1) * riemannZeta₀ s
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.size_insert_le : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (t.insert k).size ≤ t.size + 1
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Rat.instSubsingletonInfinitePlace : Subsingleton (NumberField.InfinitePlace ℚ)
-- Mathlib.Analysis.Calculus.FDeriv.Basic
differentiableWithinAt_univ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E}, DifferentiableWithinAt 𝕜 f Set.univ x ↔ DifferentiableAt 𝕜 f x
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.le_map_map_zero : ∀ (f g : CircleDeg1Lift), f 0 + ↑⌊g 0⌋ ≤ f (g 0)
-- Mathlib.Algebra.Category.MonCat.Basic
_private.Mathlib.Algebra.Category.MonCat.Basic.0.AddMonCat.Hom.mk.sizeOf_spec : ∀ {A B : AddMonCat} (hom' : ↑A →+ ↑B), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.hasForgetToMonCat.eq_1 : GrpCat.hasForgetToMonCat =
  {
    forget₂ :=
      { obj := fun X => MonCat.of ↑X, map := fun {X Y} f => MonCat.ofHom (GrpCat.Hom.hom f),
        map_id := GrpCat.hasForgetToMonCat._proof_1, map_comp := @GrpCat.hasForgetToMonCat._proof_2 },
    forget_comp := GrpCat.hasForgetToMonCat._proof_4 }
-- Mathlib.CategoryTheory.Grothendieck
/-- Making the equality of functors into an isomorphism. Note: we should avoid equality of functors
if possible, and we should prefer `map_comp_iso` to `map_comp_eq` whenever we can.  -/
CategoryTheory.Grothendieck.mapCompIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G H : CategoryTheory.Functor C CategoryTheory.Cat} →
      (α : F ⟶ G) →
        (β : G ⟶ H) →
          CategoryTheory.Grothendieck.map (CategoryTheory.CategoryStruct.comp α β) ≅
            (CategoryTheory.Grothendieck.map α).comp (CategoryTheory.Grothendieck.map β)
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.map_eq_pure_bind : ∀ {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {α β : Type w} {f : α → β}
  {x : Std.Iterators.PostconditionT m α}, Std.Iterators.PostconditionT.map f x = x.bind (pure ∘ f)
-- Mathlib.CategoryTheory.Monoidal.Types.Basic
CategoryTheory.associator_hom_apply : ∀ {X Y Z : Type u} {x : X} {y : Y} {z : Z},
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom) ((x, y), z) =
    (x, y, z)
-- Batteries.Data.Fin.Basic
/-- Sum of a tuple indexed by `Fin n`.  -/
Fin.sum : {α : Type u_1} → {n : ℕ} → [Zero α] → [Add α] → (Fin n → α) → α
-- Init.Data.Nat.Basic
Nat.lt_add_left : ∀ {a b : ℕ} (c : ℕ), a < b → a < c + b
-- Mathlib.CategoryTheory.Presentable.Adjunction
CategoryTheory.Adjunction.isCardinalFilteredGenerator : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {κ : Cardinal.{w}}
  [inst_2 : Fact κ.IsRegular] {P : CategoryTheory.ObjectProperty C},
  P.IsCardinalFilteredGenerator κ →
    ∀ [G.IsCardinalAccessible κ] [G.Full] [G.Faithful], (P.map F).IsCardinalFilteredGenerator κ
-- Init.Data.List.SplitOn.Basic
_private.Init.Data.List.SplitOn.Basic.0.List.splitOnPTR.go.eq_1 : ∀ {α : Type u_1} (p : α → Bool) (a : Array α) (a_1 : Array (List α)),
  List.splitOnPTR.go✝ p [] a a_1 = a_1.toListAppend [a.toList]
-- Init.Data.List.Basic
List.isPrefixOf.eq_3 : ∀ {α : Type u} [inst : BEq α] (a : α) (as : List α) (b : α) (bs : List α),
  (a :: as).isPrefixOf (b :: bs) = (a == b && as.isPrefixOf bs)
-- Init.Prelude
/-- If `val : α`, then `α` is nonempty.  -/
Nonempty.intro : ∀ {α : Sort u} (val : α), Nonempty α
-- Mathlib.SetTheory.Ordinal.Notation
ONote.fastGrowing_two : ONote.fastGrowing 2 = fun n => 2 ^ n * n
-- Mathlib.Topology.Algebra.GroupWithZero
/-- If a group with zero has continuous inversion, then its group of units is homeomorphic to
the set of nonzero elements.  -/
unitsHomeomorphNeZero : {G₀ : Type u_3} →
  [inst : GroupWithZero G₀] → [inst_1 : TopologicalSpace G₀] → [ContinuousInv₀ G₀] → G₀ˣ ≃ₜ { g // g ≠ 0 }
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.ofList_cons : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {k : α} {v : β} {tl : List (α × β)},
  Std.DTreeMap.Const.ofList ((k, v) :: tl) cmp = Std.DTreeMap.Const.insertMany (∅.insert k v) tl
-- Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
/-- Any nontrivial linearly ordered abelian group that is locally finite is isomorphic to `ℤ`.  -/
LocallyFiniteOrder.orderAddMonoidEquiv : (G : Type u_2) →
  [inst : AddCommGroup G] →
    [inst_1 : LinearOrder G] → [IsOrderedAddMonoid G] → [LocallyFiniteOrder G] → [Nontrivial G] → G ≃+o ℤ
-- Init.Control.Lawful.Instances
_private.Init.Control.Lawful.Instances.0.ExceptT.bindCont.match_1.eq_2 : ∀ {ε α : Type u_1} (motive : Except ε α → Sort u_2) (e : ε) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.error e with
    | Except.ok a => h_1 a
    | Except.error e => h_2 e) =
    h_2 e
-- Mathlib.RingTheory.KrullDimension.Zero
Ring.KrullDimLE.nilradical_eq_maximalIdeal : ∀ (R : Type u_1) [inst : CommSemiring R] [Ring.KrullDimLE 0 R] [inst_2 : IsLocalRing R],
  nilradical R = IsLocalRing.maximalIdeal R
-- Mathlib.Order.Basic
/-- **Alias** of `lt_of_lt_of_le`. -/
LT.lt.trans_le : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, a < b → b ≤ c → a < c
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.instIsValuedIn : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N), P.IsValuedIn R
-- Lean.DocString.Types
Lean.Doc.Block.brecOn_1.eq : ∀ {i : Type u} {b : Type v} {motive_1 : Lean.Doc.Block i b → Sort u_1}
  {motive_2 : Array (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1}
  {motive_3 : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1}
  {motive_4 : Array (Lean.Doc.Block i b) → Sort u_1}
  {motive_5 : List (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1}
  {motive_6 : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1}
  {motive_7 : List (Lean.Doc.Block i b) → Sort u_1} {motive_8 : Lean.Doc.ListItem (Lean.Doc.Block i b) → Sort u_1}
  {motive_9 : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b) → Sort u_1}
  (t : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))) (F_1 : (t : Lean.Doc.Block i b) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))) → Lean.Doc.Block.below_1 t → motive_2 t)
  (F_3 :
    (t : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) → Lean.Doc.Block.below_2 t → motive_3 t)
  (F_4 : (t : Array (Lean.Doc.Block i b)) → Lean.Doc.Block.below_3 t → motive_4 t)
  (F_5 : (t : List (Lean.Doc.ListItem (Lean.Doc.Block i b))) → Lean.Doc.Block.below_4 t → motive_5 t)
  (F_6 :
    (t : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) → Lean.Doc.Block.below_5 t → motive_6 t)
  (F_7 : (t : List (Lean.Doc.Block i b)) → Lean.Doc.Block.below_6 t → motive_7 t)
  (F_8 : (t : Lean.Doc.ListItem (Lean.Doc.Block i b)) → Lean.Doc.Block.below_7 t → motive_8 t)
  (F_9 : (t : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Lean.Doc.Block.below_8 t → motive_9 t),
  Lean.Doc.Block.brecOn_1 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 =
    F_2 t (Lean.Doc.Block.brecOn_1.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9).2
-- Mathlib.Algebra.Module.Bimodule
Subbimodule.coe_mk : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring A] [inst_4 : Semiring B] [inst_5 : Module A M] [inst_6 : Module B M]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R B M]
  [inst_11 : SMulCommClass A B M] (p : AddSubmonoid M) (hA : ∀ (a : A) {m : M}, m ∈ p → a • m ∈ p)
  (hB : ∀ (b : B) {m : M}, m ∈ p → b • m ∈ p), ↑(Subbimodule.mk p hA hB) = ↑p
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformContinuous_div : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α], UniformContinuous fun p => p.1 / p.2
-- Mathlib.Topology.ContinuousOn
/-- If a function is continuous on a set for some topologies, then it is
continuous on the same set with respect to any coarser topology on the target space.  -/
ContinuousOn.mono_rng : ∀ {α : Type u_5} {β : Type u_6} {t₁ : TopologicalSpace α} {t₂ t₃ : TopologicalSpace β},
  t₂ ≤ t₃ → ∀ {s : Set α} {f : α → β}, ContinuousOn f s → ContinuousOn f s
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.instIsIsoLeftHomFullSubcategoryOverIsMono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {A B : CategoryTheory.MonoOver X} (f : A ⟶ B)
  [CategoryTheory.IsIso f], CategoryTheory.IsIso (CategoryTheory.Over.Hom.left f.hom)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_filterMap : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w}
  [inst : Std.TransOrd α] {f : (a : α) → β a → Option (γ a)} {k : α} (h : t.WF)
  {h' : Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl = true},
  (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl.getKey k h' = t.getKey k ⋯
-- Lean.Meta.Tactic.Grind.EMatch
/-- A mapping `uniqueId ↦ thm`, where `uniqueId` is an auxiliary marker used to wrap a theorem instantiation proof of `thm`
using a `Expr.mdata`. The `uniqueId`s are created using `mkFreshId`.
 -/
Lean.Meta.Grind.EMatch.InstanceMap : Type
-- Mathlib.CategoryTheory.Monad.Comonadicity
CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv_symm_apply_f : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (A : adj.toComonad.Coalgebra) (B : C)
  [inst_2 : CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))]
  (f : B ⟶ CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointObj adj A),
  ((CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv adj A B).symm f).f =
    (adj.homEquiv B A.A).symm
      (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A))))
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.natTrailingDegree_le_natDegree : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), p.natTrailingDegree ≤ p.natDegree
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.coreOfNat.inj : ∀ {a b : Lean.Expr} {natStructId : ℕ} {lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr} {a_1 b_1 : Lean.Expr}
  {natStructId_1 : ℕ} {lhs_1 rhs_1 : Lean.Meta.Grind.Arith.Linear.LinExpr},
  Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.coreOfNat a b natStructId lhs rhs =
      Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.coreOfNat a_1 b_1 natStructId_1 lhs_1 rhs_1 →
    a = a_1 ∧ b = b_1 ∧ natStructId = natStructId_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.ofList_toList : ∀ {α : Type u_1} (xs : FreeAddMonoid α), FreeAddMonoid.ofList (FreeAddMonoid.toList xs) = xs
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.localRealizationCtxMap : Lean.Environment → Lean.NameMap Lean.RealizationContext✝
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsQF.castLE : ∀ {L : FirstOrder.Language} {α : Type u'} {n l : ℕ} {φ : L.BoundedFormula α l} {h : l ≤ n},
  φ.IsQF → (FirstOrder.Language.BoundedFormula.castLE h φ).IsQF
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.minD_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback : α}, t.minD fallback ∈ t
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct : {C : Type u_1} →
  {D : Type u_2} →
    {inst : CategoryTheory.Category.{v_1, u_1} C} →
      {inst_1 : CategoryTheory.Category.{v_2, u_2} D} →
        {inst_2 : CategoryTheory.MonoidalCategory C} →
          [self : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] →
            CategoryTheory.MonoidalCategory.MonoidalRightActionStruct C D
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
HomotopyCategory.instIsTriangulatedIntUpMapHomotopyCategory : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Limits.HasBinaryBiproducts C] [inst_4 : CategoryTheory.Preadditive D]
  [inst_5 : CategoryTheory.Limits.HasBinaryBiproducts D] [inst_6 : CategoryTheory.Limits.HasZeroObject C]
  [inst_7 : CategoryTheory.Limits.HasZeroObject D] (G : CategoryTheory.Functor C D) [inst_8 : G.Additive],
  (G.mapHomotopyCategory (ComplexShape.up ℤ)).IsTriangulated
-- Std.Data.DTreeMap.Internal.Lemmas
_private.Std.Data.DTreeMap.Internal.Lemmas.0.Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew?.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive x
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
intervalIntegral.FTCFilter.mk : ∀ {a : outParam ℝ} {outer : Filter ℝ} {inner : outParam (Filter ℝ)}
  [toTendstoIxxClass : Filter.TendstoIxxClass Set.Ioc outer inner],
  pure a ≤ outer → inner ≤ nhds a → ∀ [meas_gen : inner.IsMeasurablyGenerated], intervalIntegral.FTCFilter a outer inner
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- a morphism `S₁.X₃ ⟶ S₂.X₃`  -/
CategoryTheory.ShortComplex.Homotopy.h₃ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ₁ φ₂ : S₁ ⟶ S₂} → CategoryTheory.ShortComplex.Homotopy φ₁ φ₂ → (S₁.X₃ ⟶ S₂.X₃)
-- Mathlib.Order.Filter.Ultrafilter.Defs
Filter.isAtom_pure : ∀ {α : Type u} {a : α}, IsAtom (pure a)
-- Plausible.Random
Plausible.Random.instBoundedRandomNat : {m : Type → Type u_1} → [Monad m] → Plausible.BoundedRandom m ℕ
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.symmetry_symmetry : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C}
  {g : F.obj a ⟶ Y} (hg : F.relativelyRepresentable g) [inst_2 : F.Full] [F.Faithful],
  CategoryTheory.CategoryStruct.comp (hf'.symmetry hg) (hg.symmetry hf') =
    CategoryTheory.CategoryStruct.id (hf'.pullback g)
-- Mathlib.Algebra.Group.Prod
/-- Combine two `AddMonoidHom`s `f : M →+ N`, `g : M →+ P` into
`f.prod g : M →+ N × P` given by `(f.prod g) x = (f x, g x)`  -/
AddMonoidHom.prod : {M : Type u_3} →
  {N : Type u_4} →
    {P : Type u_5} →
      [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → [inst_2 : AddZeroClass P] → (M →+ N) → (M →+ P) → M →+ N × P
-- Mathlib.AlgebraicTopology.SimplicialObject.Op
SimplicialObject.opEquivalence_unitIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C],
  SimplicialObject.opEquivalence.unitIso = SimplicialObject.opFunctorCompOpFunctorIso.symm
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.ker_map : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] (N : AddSubgroup G) [nN : N.Normal]
  (M : AddSubgroup H) [inst_2 : M.Normal] (f : G →+ H) (h : N ≤ AddSubgroup.comap f M),
  (QuotientAddGroup.map N M f h).ker = AddSubgroup.map (QuotientAddGroup.mk' N) (AddSubgroup.comap f M)
-- Mathlib.Order.Lattice
sup_idem : ∀ {α : Type u} [inst : SemilatticeSup α] (a : α), a ⊔ a = a
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_filter_iff : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Bool},
  m.WF → ((Std.HashMap.Raw.filter f m).isEmpty = true ↔ ∀ (k : α) (h : k ∈ m), f (m.getKey k h) m[k] = false)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.abs_le_left_of_norm : ∀ (m n : ℤ), ↑|n| ≤ ‖![n, m]‖
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- Given a nonempty affine subspace, whose direction is complete,
that contains a set of points, those points are cospherical if and
only if they are equidistant from some point in that subspace.  -/
EuclideanGeometry.cospherical_iff_exists_mem_of_complete : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} {ps : Set P},
  ps ⊆ ↑s →
    ∀ [Nonempty ↥s] [s.direction.HasOrthogonalProjection],
      EuclideanGeometry.Cospherical ps ↔ ∃ center ∈ s, ∃ radius, ∀ p ∈ ps, dist p center = radius
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.sqFrom_right : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c}
  (f : C₁.Hom C₂) (i : ι), CategoryTheory.Arrow.Hom.right (f.sqFrom i) = f.next i
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.ofCoeff.sizeOf_spec : ∀ {R : Type u_8} {M : Type u_9} [inst : Semiring R] [inst_1 : SizeOf R] [inst_2 : SizeOf M] (coeff : M →₀ R),
  sizeOf (MonoidAlgebra.ofCoeff coeff) = 1 + sizeOf coeff
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.attachCodeDecls.go.match_1.eq_2 : ∀ {pu : Lean.Compiler.LCNF.Purity} (motive : Lean.Compiler.LCNF.CodeDecl pu → Sort u_1)
  (decl : Lean.Compiler.LCNF.FunDecl pu) (h : pu = Lean.Compiler.LCNF.Purity.pure)
  (h_1 : (decl : Lean.Compiler.LCNF.LetDecl pu) → motive (Lean.Compiler.LCNF.CodeDecl.let decl))
  (h_2 :
    (decl : Lean.Compiler.LCNF.FunDecl pu) →
      (h : pu = Lean.Compiler.LCNF.Purity.pure) → motive (Lean.Compiler.LCNF.CodeDecl.fun decl h))
  (h_3 : (decl : Lean.Compiler.LCNF.FunDecl pu) → motive (Lean.Compiler.LCNF.CodeDecl.jp decl))
  (h_4 :
    (fvarId : Lean.FVarId) →
      (idx : ℕ) →
        (y : Lean.Compiler.LCNF.Arg pu) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.oset fvarId idx y h))
  (h_5 :
    (fvarId : Lean.FVarId) →
      (idx : ℕ) →
        (y : Lean.FVarId) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.uset fvarId idx y h))
  (h_6 :
    (fvarId : Lean.FVarId) →
      (idx offset : ℕ) →
        (y : Lean.FVarId) →
          (ty : Lean.Expr) →
            (h : pu = Lean.Compiler.LCNF.Purity.impure) →
              motive (Lean.Compiler.LCNF.CodeDecl.sset fvarId idx offset y ty h))
  (h_7 :
    (fvarId : Lean.FVarId) →
      (cidx : ℕ) →
        (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.setTag fvarId cidx h))
  (h_8 :
    (fvarId : Lean.FVarId) →
      (n : ℕ) →
        (check persistent : Bool) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) →
            motive (Lean.Compiler.LCNF.CodeDecl.inc fvarId n check persistent h))
  (h_9 :
    (fvarId : Lean.FVarId) →
      (n : ℕ) →
        (check persistent : Bool) →
          (objs? : Option ℕ) →
            (h : pu = Lean.Compiler.LCNF.Purity.impure) →
              motive (Lean.Compiler.LCNF.CodeDecl.dec fvarId n check persistent objs? h))
  (h_10 :
    (fvarId : Lean.FVarId) →
      (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.del fvarId h)),
  (match Lean.Compiler.LCNF.CodeDecl.fun decl h with
    | Lean.Compiler.LCNF.CodeDecl.let decl => h_1 decl
    | Lean.Compiler.LCNF.CodeDecl.fun decl h => h_2 decl h
    | Lean.Compiler.LCNF.CodeDecl.jp decl => h_3 decl
    | Lean.Compiler.LCNF.CodeDecl.oset fvarId idx y h => h_4 fvarId idx y h
    | Lean.Compiler.LCNF.CodeDecl.uset fvarId idx y h => h_5 fvarId idx y h
    | Lean.Compiler.LCNF.CodeDecl.sset fvarId idx offset y ty h => h_6 fvarId idx offset y ty h
    | Lean.Compiler.LCNF.CodeDecl.setTag fvarId cidx h => h_7 fvarId cidx h
    | Lean.Compiler.LCNF.CodeDecl.inc fvarId n check persistent h => h_8 fvarId n check persistent h
    | Lean.Compiler.LCNF.CodeDecl.dec fvarId n check persistent objs? h => h_9 fvarId n check persistent objs? h
    | Lean.Compiler.LCNF.CodeDecl.del fvarId h => h_10 fvarId h) =
    h_2 decl h
-- Lean.Elab.DocString
/-- Gadget that indicates that a function's parameter should be treated as a repeated (and thus
optional) named argument when used in a docstring extension.
 -/
Lean.Doc.many : Type u → Type u
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Lean.Meta.Grind.Arith.Cutsat.getVars : Lean.Meta.Grind.GoalM (Lean.PArray Lean.Expr)
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
/-- The inverse of a localizer morphism `Φ : LocalizerMorphism W₁ W₂`,
when `Φ.functor` is an equivalence, `W₁` is induced by `W₂`
and `W₂` respects isomorphisms.  -/
CategoryTheory.LocalizerMorphism.inv : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) →
              [Φ.functor.IsEquivalence] → [Φ.IsInduced] → [W₂.RespectsIso] → CategoryTheory.LocalizerMorphism W₂ W₁