mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKeyD_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {km fallback : α}, t.minKeyD fallback = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Topology.Constructions.SumProd
isQuotientMap_fst : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [Nonempty Y],
  Topology.IsQuotientMap Prod.fst
-- Mathlib.Analysis.Asymptotics.ExpGrowth
Monotone.expGrowthSup_comp_mul : ∀ {u : ℕ → ENNReal} {m : ℕ},
  Monotone u → m ≠ 0 → (ExpGrowth.expGrowthSup fun n => u (m * n)) = ↑m * ExpGrowth.expGrowthSup u
-- Mathlib.Order.BourbakiWitt
/-- **The Bourbaki-Witt Theorem**: If `α` is a chain complete partial order and `f : α → α` is
inflationary, then `f` has a fixed point  -/
ChainCompletePartialOrder.nonempty_fixedPoints_of_inflationary : ∀ {α : Type u_1} [inst : ChainCompletePartialOrder α] {f : α → α} [Nonempty α],
  (∀ (x : α), x ≤ f x) → (Function.fixedPoints f).Nonempty
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.postcomposing₂_obj_naturality_hom_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b : B) (f : a ⟶ b) {a_1 b_1 : Bᵒᵖ} (g : a_1 ⟶ b_1)
  (X : ↑(CategoryTheory.Cat.of (Opposite.unop a_1 ⟶ a))),
  (((CategoryTheory.Bicategory.postcomposing₂ a b).obj f).naturality g).hom.toNatTrans.app X =
    (CategoryTheory.Bicategory.associator g.unop X f).hom
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.map_hom_inv_id_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {X Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C D) {Z : D} (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map e.hom) (CategoryTheory.CategoryStruct.comp (F.map e.inv) h) = h
-- Mathlib.Data.List.Duplicate
List.Duplicate.mem_cons_self : ∀ {α : Type u_1} {l : List α} {x : α}, List.Duplicate x (x :: l) → x ∈ l
-- Init.Data.BitVec.Lemmas
BitVec.setWidth_ushiftRight : ∀ {w i : ℕ} {x : BitVec w} {y : ℕ}, w ≤ i → BitVec.setWidth i (x >>> y) = BitVec.setWidth i x >>> y
-- Mathlib.Order.Closure
LowerAdjoint.closure_union_closure_subset : ∀ {α : Type u_1} {β : Type u_4} [inst : SetLike α β] [inst_1 : Preorder α] (l : LowerAdjoint SetLike.coe) (x y : α),
  ↑(l.toFun ↑x) ∪ ↑(l.toFun ↑y) ⊆ ↑(l.toFun (↑x ∪ ↑y))
-- Mathlib.Algebra.Tropical.Basic
/-- The tropicalization of a type `R`.  -/
Tropical : Type u → Type u
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_eq_zero_of_nonpos : ∀ {x : ℝ}, x ≤ 0 → √x = 0
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.mk : {α : Type u} → [inst : AddMonoid α] → (val neg : α) → val + neg = 0 → neg + val = 0 → AddUnits α
-- Mathlib.Data.Int.Interval
Finset.Icc_succ_succ : ∀ (m n : ℕ), Finset.Icc (-(↑m + 1)) (↑n + 1) = Finset.Icc (-↑m) ↑n ∪ {-(↑m + 1), ↑n + 1}
-- Mathlib.Algebra.Lie.Classical
/-- An equivalence between the indefinite and definite orthogonal Lie algebras, over a ring
containing a square root of -1.  -/
LieAlgebra.Orthogonal.soIndefiniteEquiv : (p : Type u_2) →
  (q : Type u_3) →
    (R : Type u₂) →
      [inst : DecidableEq p] →
        [inst_1 : DecidableEq q] →
          [inst_2 : CommRing R] →
            [inst_3 : Fintype p] →
              [inst_4 : Fintype q] →
                {i : R} → i * i = -1 → ↥(LieAlgebra.Orthogonal.so' p q R) ≃ₗ⁅R⁆ ↥(LieAlgebra.Orthogonal.so (p ⊕ q) R)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.codRestrict.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {S : Type u_5} [inst_2 : SetLike S N]
  [inst_3 : AddSubmonoidClass S N] (f : M →+ N) (s : S) (h : ∀ (x : M), f x ∈ s),
  f.codRestrict s h = { toFun := fun n => ⟨f n, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.map_toDeleteEdges_eq : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} (s : Set (Sym2 V)) {p : G.Walk v w} (hp : ∀ e ∈ p.edges, e ∉ s),
  SimpleGraph.Walk.map (SimpleGraph.Hom.ofLE ⋯) (SimpleGraph.Walk.toDeleteEdges s p hp) = p
-- Mathlib.Data.Finsupp.Lex
Finsupp.Lex.isBotZeroClass : ∀ {α : Type u_1} {N : Type u_2} [inst : LinearOrder α] [inst_1 : AddCommMonoid N] [inst_2 : PartialOrder N]
  [IsBotZeroClass N], IsBotZeroClass (Lex (α →₀ N))
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succ.congr_simp : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.InfinitelyUpwardEnumerable α] (a a_1 : α),
  a = a_1 → Std.PRange.succ a = Std.PRange.succ a_1
-- Mathlib.ModelTheory.Syntax
/-- The sentence indicating that a basic relation symbol is irreflexive.  -/
FirstOrder.Language.Relations.irreflexive : {L : FirstOrder.Language} → L.Relations 2 → L.Sentence
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.nsmul_empty : ∀ {α : Type u_2} [inst : AddMonoid α] {n : ℕ}, n ≠ 0 → n • ∅ = ∅
-- Mathlib.CategoryTheory.Equivalence.Symmetry
/-- Promoting `Equivalence.congrLeft` to a functor.  -/
CategoryTheory.Equivalence.congrLeftFunctor : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (D : Type u_2) →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (E : Type u_3) →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
            CategoryTheory.Functor (C ≌ D) (CategoryTheory.Functor C E ≌ CategoryTheory.Functor D E)ᵒᵖ
-- Mathlib.Combinatorics.Enumerative.Composition
List.splitWrtCompositionAux_cons : ∀ {α : Type u_1} (l : List α) (n : ℕ) (ns : List ℕ),
  l.splitWrtCompositionAux (n :: ns) = List.take n l :: (List.drop n l).splitWrtCompositionAux ns
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.map_right_cancel : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) {x y : M} {c : ↥S}, f (↑c * x) = f (↑c * y) → f x = f y
-- Mathlib.CategoryTheory.Monad.Coequalizer
CategoryTheory.Monad.FreeCoequalizer.topMap_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra),
  (CategoryTheory.Monad.FreeCoequalizer.topMap X).f = T.map X.a
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.sumEmpty_toEquiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_5} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_9}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} {M' : Type u_13}
  [inst_6 : TopologicalSpace M'] [inst_7 : ChartedSpace H M'] [inst_8 : IsEmpty M'],
  (Diffeomorph.sumEmpty I M n).toEquiv = Equiv.sumEmpty M M'
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_insertMany_empty_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} [Std.TransOrd α] [inst : BEq α] [Std.LawfulBEqOrd α]
  [inst_2 : Std.LawfulEqOrd α] {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (↑(Std.DTreeMap.Internal.Impl.empty.insertMany l ⋯)).get? k = none
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.coe_id : ∀ {X : AddGrpCat}, ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.map : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashMap.Raw α β},
  m₁.WF → m₂.WF → ∀ (f : α → β → γ), m₁.Equiv m₂ → (Std.HashMap.Raw.map f m₁).Equiv (Std.HashMap.Raw.map f m₂)
-- Mathlib.Topology.ContinuousMap.Units
ContinuousMap.isUnit_iff_forall_ne_zero : ∀ {X : Type u_1} {R : Type u_3} [inst : TopologicalSpace X] [inst_1 : NormedDivisionRing R] [CompleteSpace R]
  (f : C(X, R)), IsUnit f ↔ ∀ (x : X), f x ≠ 0
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  (t₁ ∩ t₂).get? k = if k ∈ t₂ then t₁.get? k else none
-- Init.Data.List.Basic
List.zipIdx_cons : ∀ {α : Type u_1} {a : α} {as : List α} {i : ℕ}, (a :: as).zipIdx i = (a, i) :: as.zipIdx (i + 1)
-- Mathlib.Algebra.BigOperators.Finprod
/-- If `s : Set α` and `t : Set β` are finite sets, then taking the product over `s` commutes with
taking the product over `t`.  -/
finprod_mem_comm : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] {s : Set α} {t : Set β} (f : α → β → M),
  s.Finite →
    t.Finite → ∏ᶠ (i : α) (_ : i ∈ s) (j : β) (_ : j ∈ t), f i j = ∏ᶠ (j : β) (_ : j ∈ t) (i : α) (_ : i ∈ s), f i j
-- Init.Data.Vector.Basic
Vector.foldrM : {m : Type u_1 → Type u_2} → {α : Type u_3} → {β : Type u_1} → {n : ℕ} → [Monad m] → (α → β → m β) → β → Vector α n → m β
-- Mathlib.Topology.NhdsWithin
tendsto_nhdsWithin_mono_left : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → β} {a : α} {s t : Set α} {l : Filter β},
  s ⊆ t → Filter.Tendsto f (nhdsWithin a t) l → Filter.Tendsto f (nhdsWithin a s) l
-- Mathlib.Computability.Primrec.Basic
Primrec.nat_mul : Primrec₂ fun x1 x2 => x1 * x2
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.ofFinset.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] (E : Set α) (Indep : Finset α → Prop) (indep_empty : Indep ∅)
  (indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I)
  (indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I))
  (subset_ground : ∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E),
  IndepMatroid.ofFinset E Indep indep_empty indep_subset indep_aug subset_ground =
    IndepMatroid.ofFinitaryCardAugment E (fun I => ∀ (J : Finset α), ↑J ⊆ I → Indep J) ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.Γ_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : (AlgebraicGeometry.PresheafedSpace C)ᵒᵖ}
  (f : X ⟶ Y), AlgebraicGeometry.PresheafedSpace.Γ.map f = f.unop.c.app (Opposite.op ⊤)
-- Lean.Expr
/-- Given `a b : Nat`, return `a = b`  -/
Lean.mkNatEq : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Topology.Algebra.Ring.Real
instIsTopologicalDivisionRingReal : IsTopologicalDivisionRing ℝ
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- The circumradius of a triangle may be expressed explicitly as half the length of a side
divided by the absolute value of the sine of the angle at the third point (a version of the law
of sines or sine rule).  -/
Affine.Triangle.dist_div_sin_oangle_div_two_eq_circumradius : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ →
      i₂ ≠ i₃ →
        dist (t.points i₁) (t.points i₃) / |(EuclideanGeometry.oangle (t.points i₁) (t.points i₂) (t.points i₃)).sin| /
            2 =
          Affine.Simplex.circumradius t
-- Mathlib.Data.Finsupp.Basic
Finsupp.piecewise_apply : ∀ {α : Type u_1} {M : Type u_12} [inst : Zero M] {P : α → Prop} [inst_1 : DecidablePred P] (f : Subtype P →₀ M)
  (g : { a // ¬P a } →₀ M) (a : α), (f.piecewise g) a = if h : P a then f ⟨a, h⟩ else g ⟨a, h⟩
-- Lean.Elab.App
Lean.Elab.Term.ElabAppArgs.State.mk.injEq : ∀ (f fType : Lean.Expr) (fArgs : Array Lean.Expr) (args : List Lean.Elab.Term.Arg)
  (namedArgs : List Lean.Elab.Term.NamedArg) (expectedType? : Option Lean.Expr)
  (etaArgs : Array (Lean.Name × Lean.Expr)) (toSetErrorCtx instMVars : Array Lean.MVarId) (propagateExpected : Bool)
  (resultTypeOutParam? : Option Lean.MVarId) (foundNamedArgs : Array Lean.Name) (f_1 fType_1 : Lean.Expr)
  (fArgs_1 : Array Lean.Expr) (args_1 : List Lean.Elab.Term.Arg) (namedArgs_1 : List Lean.Elab.Term.NamedArg)
  (expectedType?_1 : Option Lean.Expr) (etaArgs_1 : Array (Lean.Name × Lean.Expr))
  (toSetErrorCtx_1 instMVars_1 : Array Lean.MVarId) (propagateExpected_1 : Bool)
  (resultTypeOutParam?_1 : Option Lean.MVarId) (foundNamedArgs_1 : Array Lean.Name),
  ({ f := f, fType := fType, fArgs := fArgs, args := args, namedArgs := namedArgs, expectedType? := expectedType?,
        etaArgs := etaArgs, toSetErrorCtx := toSetErrorCtx, instMVars := instMVars,
        propagateExpected := propagateExpected, resultTypeOutParam? := resultTypeOutParam?,
        foundNamedArgs := foundNamedArgs } =
      { f := f_1, fType := fType_1, fArgs := fArgs_1, args := args_1, namedArgs := namedArgs_1,
        expectedType? := expectedType?_1, etaArgs := etaArgs_1, toSetErrorCtx := toSetErrorCtx_1,
        instMVars := instMVars_1, propagateExpected := propagateExpected_1,
        resultTypeOutParam? := resultTypeOutParam?_1, foundNamedArgs := foundNamedArgs_1 }) =
    (f = f_1 ∧
      fType = fType_1 ∧
        fArgs = fArgs_1 ∧
          args = args_1 ∧
            namedArgs = namedArgs_1 ∧
              expectedType? = expectedType?_1 ∧
                etaArgs = etaArgs_1 ∧
                  toSetErrorCtx = toSetErrorCtx_1 ∧
                    instMVars = instMVars_1 ∧
                      propagateExpected = propagateExpected_1 ∧
                        resultTypeOutParam? = resultTypeOutParam?_1 ∧ foundNamedArgs = foundNamedArgs_1)
-- Mathlib.CategoryTheory.GlueData
/-- The transition maps between the intersections.  -/
CategoryTheory.GlueData'.t : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v, u₁} C] →
    (self : CategoryTheory.GlueData' C) → (i j : self.J) → (h : i ≠ j) → self.V i j h ⟶ self.V j i ⋯
-- Mathlib.Data.Nat.Cast.Field
Nat.cast_div : ∀ {K : Type u_1} [inst : DivisionSemiring K] {m n : ℕ}, n ∣ m → ↑n ≠ 0 → ↑(m / n) = ↑m / ↑n
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.coe_toBoundedOrderHom : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] (f : BoundedLatticeHom α β), ⇑f.toBoundedOrderHom = ⇑f
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Algebra.Generators.cMulXSubOneCotangent_eq : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (r : R)
  [inst_3 : IsLocalization.Away r S],
  Algebra.Generators.cMulXSubOneCotangent S r =
    Algebra.Extension.Cotangent.mk ⟨MvPolynomial.C r * MvPolynomial.X () - 1, ⋯⟩
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Term.realize_constantsVarsEquivLeft : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {β : Type v'}
  [inst_1 : (L.withConstants α).Structure M] [(L.lhomWithConstants α).IsExpansionOn M] {n : ℕ}
  {t : (L.withConstants α).Term (β ⊕ Fin n)} {v : β → M} {xs : Fin n → M},
  FirstOrder.Language.Term.realize (Sum.elim (Sum.elim (fun a => ↑(L.con a)) v) xs)
      (FirstOrder.Language.Term.constantsVarsEquivLeft t) =
    FirstOrder.Language.Term.realize (Sum.elim v xs) t
-- Init.Data.SInt.Lemmas
Int8.toInt_toISize : ∀ (x : Int8), x.toISize.toInt = x.toInt
-- Mathlib.CategoryTheory.RegularCategory.Basic
CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation_m : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Regular C] {A B : C} (f : A ⟶ B)
  (A' : CategoryTheory.Subobject A) (B' : CategoryTheory.Subobject B),
  (CategoryTheory.Regular.frobeniusStrongEpiMonoFactorisation f A' B').m =
    ((CategoryTheory.Subobject.exists f).obj A' ⊓ B').arrow
-- Init.Data.Range.Polymorphic.Map
Std.Rxc.LawfulHasSize.ofMap : ∀ {α : Type u_1} {β : Type u_2} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.UpwardEnumerable β]
  [inst_2 : LE α] [inst_3 : LE β] [inst_4 : Std.Rxc.HasSize α] [inst_5 : Std.Rxc.HasSize β] [Std.Rxc.LawfulHasSize β]
  (f : Std.PRange.UpwardEnumerable.Map α β) [f.PreservesLE] [f.PreservesRxcSize], Std.Rxc.LawfulHasSize α
-- Mathlib.Order.SuccPred.LinearLocallyFinite
/-- A locally finite order is a `PredOrder`.
This is not an instance, because its `succ` field conflicts with computable `PredOrder` structures
on `ℕ` and `ℤ`.  -/
LinearLocallyFiniteOrder.predOrder : (ι : Type u_1) → [inst : LinearOrder ι] → [LocallyFiniteOrder ι] → PredOrder ι
-- Batteries.Data.BitVec.Lemmas
/-- **Alias** of `BitVec.getMsb_ofFnLE`. -/
BitVec.getMsb'_ofFnLE : ∀ {n : ℕ} (f : Fin n → Bool) (i : Fin n), (BitVec.ofFnLE f).getMsb i = f i.rev
-- Init.Data.List.Basic
List.dropLast.eq_def : ∀ {α : Type u_1} (x : List α),
  x.dropLast =
    match x with
    | [] => []
    | [head] => []
    | a :: as => a :: as.dropLast
-- Mathlib.Order.Monotone.Basic
monotone_nat_of_le_succ : ∀ {α : Type u} [inst : Preorder α] {f : ℕ → α}, (∀ (n : ℕ), f n ≤ f (n + 1)) → Monotone f
-- Init.Grind.Offset
Lean.Grind.Nat.unsat_le_lo : ∀ (u v k : ℕ), Lean.Grind.isLt 0 k = true → u ≤ v → v + k ≤ u → False
-- Lean.Meta.Match.Basic
Lean.Meta.Match.congrEqnThmSuffixBasePrefix : String
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.Input.mk : {ι : Type} →
  {elem idx : outParam Type} →
    [inst : DecidableEq idx] →
      [inst_1 : DecidableEq elem] →
        (ι → idx) →
          (ι → ι) →
            (ι → elem) →
              (hasNext : ι → Bool) →
                ((it : ι) → hasNext it = true → ι) →
                  ((it : ι) → hasNext it = true → elem) → Std.Internal.Parsec.Input ι elem idx
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
AddMonoidAlgebra.toDirectSum_natCast : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : Semiring M] (n : ℕ),
  (↑n).toDirectSum = ↑n
-- Init.Data.Iterators.Basic
Std.IterM.IsPlausibleIndirectSuccessorOf.below.refl : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] {a : Std.IterM m β}
  {motive : (a_1 : Std.IterM m β) → a.IsPlausibleIndirectSuccessorOf a_1 → Prop},
  Std.IterM.IsPlausibleIndirectSuccessorOf.below ⋯
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse.eq_1 : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] (W : CategoryTheory.MorphismProperty C) (D : Type uD)
  [inst_1 : CategoryTheory.Category.{uD', uD} D],
  CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse W D =
    { obj := fun G => CategoryTheory.Localization.Construction.lift G.obj ⋯,
      map := fun {X Y} τ =>
        CategoryTheory.Localization.Construction.natTransExtension
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp τ.hom (CategoryTheory.eqToHom ⋯))),
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Topology.MetricSpace.Thickening
Bornology.IsBounded.thickening : ∀ {X : Type u} [inst : PseudoMetricSpace X] {δ : ℝ} {E : Set X},
  Bornology.IsBounded E → Bornology.IsBounded (Metric.thickening δ E)
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
Bundle.Trivialization.contMDiffWithinAt_snd_comp_iff₂ : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6}
  [inst : NontriviallyNormedField 𝕜] {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB]
  {HB : Type u_8} [inst_3 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] {EM : Type u_9} [inst_6 : NormedAddCommGroup EM] [inst_7 : NormedSpace 𝕜 EM]
  {HM : Type u_10} [inst_8 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace HM M] [inst_11 : (x : B) → AddCommMonoid (E x)] [inst_12 : (x : B) → Module 𝕜 (E x)]
  [inst_13 : NormedAddCommGroup F] [inst_14 : NormedSpace 𝕜 F] [inst_15 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_16 : (x : B) → TopologicalSpace (E x)] [inst_17 : FiberBundle F E] [inst_18 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle n F E IB] {e e' : Bundle.Trivialization F Bundle.TotalSpace.proj} [MemTrivializationAtlas e]
  [MemTrivializationAtlas e'] {s : Set M} {x : M} {f : M → Bundle.TotalSpace F E},
  ContMDiffWithinAt IM IB n (Bundle.TotalSpace.proj ∘ f) s x →
    f x ∈ e.source →
      f x ∈ e'.source →
        (ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 F) n (fun y => (↑e (f y)).2) s x ↔
          ContMDiffWithinAt IM (modelWithCornersSelf 𝕜 F) n (fun y => (↑e' (f y)).2) s x)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.fixingAddSubgroup_union_to_fixingAddSubgroup_of_fixingAddSubgroup.eq_1 : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {s t : Set α},
  SubAddAction.fixingAddSubgroup_union_to_fixingAddSubgroup_of_fixingAddSubgroup =
    { toFun := fun m => ⟨⟨↑m, ⋯⟩, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }
-- Init.Data.Bool
Bool.xor_not_self : ∀ (x : Bool), (x ^^ !x) = true
-- Mathlib.Algebra.Quaternion
Quaternion.re_neg : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), (-a).re = -a.re
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Measurable.eq : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : MeasurableSpace β] [MeasurableEq β] {f g : α → β},
  Measurable f → Measurable g → Measurable fun x => f x = g x
-- Lean.Meta.AppBuilder
Lean.Meta.mkEqNDRec : Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Computability.TuringMachine.Tape
/-- Construct a setoid instance for `BlankRel`.  -/
Turing.BlankRel.setoid : (Γ : Type u_1) → [Inhabited Γ] → Setoid (List Γ)
-- Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
ordinaryHypergeometric.congr_simp : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : Field 𝕂] [inst_1 : Ring 𝔸] [inst_2 : Algebra 𝕂 𝔸] [inst_3 : TopologicalSpace 𝔸]
  [inst_4 : IsTopologicalRing 𝔸] (a a_1 : 𝕂),
  a = a_1 → ∀ (b b_1 : 𝕂), b = b_1 → ∀ (c c_1 : 𝕂), c = c_1 → ∀ (x x_1 : 𝔸), x = x_1 → ₂F₁ a b c x = ₂F₁ a_1 b_1 c_1 x_1
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.instInhabitedResult : {u : Lean.Level} → {α : Q(Type u)} → {x : Q(«$α»)} → Inhabited (Mathlib.Meta.NormNum.Result x)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.equivComma_functor_map_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {X Y : CategoryTheory.Functor (CategoryTheory.WithInitial C) D} (η : X ⟶ Y),
  (CategoryTheory.WithInitial.equivComma.functor.map η).left = η.app CategoryTheory.WithInitial.star
-- Mathlib.Data.Finsupp.Defs
Finsupp.ofSupportFinite_support : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] {f : α → M} (hf : (Function.support f).Finite),
  (Finsupp.ofSupportFinite f hf).support = hf.toFinset
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.const_mul_right' : ∀ {α : Type u_1} {E : Type u_3} {R : Type u_13} [inst : Norm E] [inst_1 : SeminormedRing R] {f : α → E} {l : Filter α}
  {g : α → R} {c : R}, IsUnit c → f =o[l] g → f =o[l] fun x => c * g x
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.instLocallyConvexSpace : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul 𝕜₂ F] [inst_10 : NormedSpace ℝ 𝕜₂] [inst_11 : Module ℝ (E →SWOT[σ] F)]
  [IsScalarTower ℝ 𝕜₂ (E →SWOT[σ] F)], LocallyConvexSpace ℝ (E →SWOT[σ] F)
-- Mathlib.Combinatorics.Enumerative.DyckWord
instDecidableEqDyckWord : DecidableEq DyckWord
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.prod_const : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (μ : MeasureTheory.Measure β) [MeasureTheory.SFinite μ] (ν : MeasureTheory.Measure γ)
  [MeasureTheory.SFinite ν],
  (ProbabilityTheory.Kernel.const α μ).prod (ProbabilityTheory.Kernel.const α ν) =
    ProbabilityTheory.Kernel.const α (μ.prod ν)
-- Init.Util
dbgSleep : {α : Type u} → UInt32 → (Unit → α) → α
-- Mathlib.Algebra.Ring.CompTypeclasses
/-- The morphisms form a commutative triangle  -/
RingHomCompTriple.comp_eq : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {inst : Semiring R₁} {inst_1 : Semiring R₂} {inst_2 : Semiring R₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : outParam (R₁ →+* R₃)} [self : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃],
  σ₂₃.comp σ₁₂ = σ₁₃