mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Maps.Proper.UniversallyClosed
/-- A map `f : X → Y` is proper if and only if it is continuous and **universally closed**, in the
sense that for any topological space `Z`, the map `Prod.map f id : X × Z → Y × Z` is closed. Note
that `Z` lives in the same universe as `X` here, but `IsProperMap.universally_closed` does not
have this restriction.

This is taken as the definition of properness in
[N. Bourbaki, *General Topology*][bourbaki1966].  -/
isProperMap_iff_universally_closed : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsProperMap f ↔ Continuous f ∧ ∀ (Z : Type u) [inst_2 : TopologicalSpace Z], IsClosedMap (Prod.map f id)
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_zsmul_const : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : AddGroup G]
  [inst_2 : AddGroup H] [AddConstMapClass F G H a b] (f : F) (n : ℤ), f (n • a) = f 0 + n • b
-- Mathlib.RingTheory.Etale.Basic
Algebra.FormallyEtale.mk : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Subsingleton Ω[A⁄R] → Subsingleton (Algebra.H1Cotangent R A) → Algebra.FormallyEtale R A
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_map : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {γ : α → Type w}
  [inst_2 : LawfulBEq α] {f : (a : α) → β a → γ a} {k : α},
  m.WF → (Std.DHashMap.Raw.map f m).get? k = Option.map (f k) (m.get? k)
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Module.finrank_eq_nat_card_basis : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type w}
  [StrongRankCondition R] (h : Module.Basis ι R M), Module.finrank R M = Nat.card ι
-- Mathlib.CategoryTheory.Yoneda
/-- The Yoneda embedding is fully faithful.  -/
CategoryTheory.Yoneda.fullyFaithful : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.yoneda.FullyFaithful
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.Const.alterKey.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((v : β) → motive (some v)) → motive x
-- Mathlib.AlgebraicGeometry.Limits
/-- `Spec ℤ` is the terminal object in the category of schemes.  -/
AlgebraicGeometry.specZIsTerminal : CategoryTheory.Limits.IsTerminal (AlgebraicGeometry.Spec (CommRingCat.of ℤ))
-- Mathlib.Geometry.Group.Growth.LinearLowerBound
Finset.pow_ssubset_pow_succ_of_pow_ne_closure : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {X : Finset G} {n : ℕ},
  1 ∈ X → X.Nontrivial → ↑X ^ n ≠ ↑(Subgroup.closure ↑X) → X ^ n ⊂ X ^ (n + 1)
-- Init.Data.List.Lemmas
List.exists_of_mem_flatMap : ∀ {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : α → List β}, b ∈ List.flatMap f l → ∃ a ∈ l, b ∈ f a
-- Mathlib.CategoryTheory.Discrete.SumsProducts
_private.Mathlib.CategoryTheory.Discrete.SumsProducts.0.CategoryTheory.sum.match_3.eq_2 : ∀ (C : Type u_1) (D : Type u_2) (motive : C ⊕ D → Sort u_3) (X : D) (h_1 : (X : C) → motive (Sum.inl X))
  (h_2 : (X : D) → motive (Sum.inr X)),
  (match Sum.inr X with
    | Sum.inl X => h_1 X
    | Sum.inr X => h_2 X) =
    h_2 X
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.add_apply : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Add α] (A B : Matrix m n α) (i : m) (j : n),
  (A + B) i j = A i j + B i j
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.natDegree_prod_of_monic : ∀ {R : Type u} {ι : Type w} (s : Finset ι) [inst : CommSemiring R] (f : ι → Polynomial R),
  (∀ i ∈ s, (f i).Monic) → (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree
-- Init.Data.AC
Lean.Data.AC.Context.idem : {α : Sort u} → (self : Lean.Data.AC.Context α) → Option (PLift (Std.IdempotentOp self.op))
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If the coproduct of `X` and `Y` exists, then every pair of morphisms `f : X ⟶ W` and
`g : Y ⟶ W` induces a morphism `l : X ⨿ Y ⟶ W` satisfying `coprod.inl ≫ l = f` and
`coprod.inr ≫ l = g`.  -/
CategoryTheory.Limits.coprod.desc' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X Y] →
        (f : X ⟶ W) →
          (g : Y ⟶ W) →
            { l //
              CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl l = f ∧
                CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr l = g }
-- Mathlib.Order.CountableDenseLinearOrder
/-- The type of partial order isomorphisms between `α` and `β` defined on finite subsets.
A partial order isomorphism is encoded as a finite subset of `α × β`, consisting
of pairs which should be identified.  -/
Order.PartialIso : (α : Type u_1) → (β : Type u_2) → [LinearOrder α] → [LinearOrder β] → Type (max u_1 u_2)
-- Mathlib.Algebra.Module.Lattice
/-- The intersection of two lattices is a lattice.  -/
Submodule.IsLattice.inf : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K] {V : Type u_3}
  [inst_3 : AddCommGroup V] [inst_4 : Module K V] [inst_5 : Module R V] [inst_6 : IsScalarTower R K V] [IsDomain R]
  [IsPrincipalIdealRing R] [Module.Finite K V] [IsFractionRing R K] (M N : Submodule R V) [Submodule.IsLattice K M]
  [Submodule.IsLattice K N], Submodule.IsLattice K (M ⊓ N)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- **Alias** of `FunLike.coe_sum`. -/
MeasureTheory.VectorMeasure.coe_finsetSum : ∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} {ι : Type u_11} [inst : FunLike F α β] [inst_1 : AddCommMonoid β]
  [inst_2 : AddCommMonoid F] [IsZeroApply F α β] [IsAddApply F α β] (s : Finset ι) (f : ι → F),
  ⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i)
-- Mathlib.Algebra.Lie.Weights.Killing
IsSl2Triple.h_eq_coroot : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] [CharZero K]
  {α : LieModule.Weight K (↥H) L},
  α.IsNonZero →
    ∀ {h e f : L},
      IsSl2Triple h e f →
        e ∈ LieAlgebra.rootSpace H ⇑α → f ∈ LieAlgebra.rootSpace H (-⇑α) → h = ↑(LieAlgebra.IsKilling.coroot α)
-- Lean.Meta.NatInstTesters
Lean.Meta.Structural.isInstHAddNat : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Order.Atoms
IsCoatom.of_isCoatom_coe_Ici : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : OrderTop α] {x : α} {a : ↑(Set.Ici x)}, IsCoatom a → IsCoatom ↑a
-- Mathlib.Analysis.RCLike.Basic
RCLike.lt_iff_re_im : ∀ {K : Type u_1} [inst : RCLike K] {z w : K}, z < w ↔ RCLike.re z < RCLike.re w ∧ RCLike.im z = RCLike.im w
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RocSlice : (α : Type u_1) → Type u_2 → [Ord α] → Type (max u_2 u_1)
-- Lean.Declaration
Lean.Declaration.thmDecl : Lean.TheoremVal → Lean.Declaration
-- Lean.Meta.Sorry
/-- Evaluates `fn` on each `sorry` in the expression.
Instantiates bound variables with free variables.
 -/
Lean.Meta.forEachSorryM : {m : Type → Type} →
  [Monad m] → [MonadLiftT Lean.MetaM m] → [MonadControlT Lean.MetaM m] → Lean.Expr → (Lean.Expr → m Unit) → m Unit
-- Mathlib.Algebra.BigOperators.Finprod
/-- Given a finite set `t` and a subset `s` of `t`, the sum of `f i` over `i ∈ s` plus
the sum of `f i` over `t \ s` equals the sum of `f i` over `i ∈ t`.  -/
finsum_mem_add_sdiff : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s t : Set α},
  s ⊆ t → t.Finite → ∑ᶠ (i : α) (_ : i ∈ s), f i + ∑ᶠ (i : α) (_ : i ∈ t \ s), f i = ∑ᶠ (i : α) (_ : i ∈ t), f i
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.IsLocallyDirected.cocone.eq_1 : ∀ {J : Type w} [inst : CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme)
  [inst_1 : ∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)]
  [inst_2 : (F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] [inst_3 : Quiver.IsThin J]
  [inst_4 : Small.{u, w} J],
  AlgebraicGeometry.Scheme.IsLocallyDirected.cocone F =
    { pt := (AlgebraicGeometry.Scheme.IsLocallyDirected.glueData F).glued,
      ι :=
        {
          app := fun j =>
            CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.eqToHom ⋯))
              ((AlgebraicGeometry.Scheme.IsLocallyDirected.glueData F).ι ((equivShrink J) j)),
          naturality := ⋯ } }
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.RingExpr : Type
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.LeAtTop.le_atTop : ∀ {β : Type u_2} {L : SummationFilter β} [self : L.LeAtTop], L.filter ≤ Filter.atTop
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- Constructor for morphisms in `ComposableArrows C 0`.  -/
CategoryTheory.ComposableArrows.homMk₀ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {F G : CategoryTheory.ComposableArrows C 0} →
      (F.obj' 0 CategoryTheory.ComposableArrows.homMk₀._proof_1 ⟶
          G.obj' 0 CategoryTheory.ComposableArrows.homMk₀._proof_1) →
        (F ⟶ G)
-- Mathlib.Algebra.Module.Equiv.Basic
/-- Between two zero modules, the zero map is the only equivalence.  -/
LinearEquiv.instUnique : {R : Type u_1} →
  {R₂ : Type u_2} →
    {M : Type u_5} →
      {M₂ : Type u_7} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R₂ M₂] →
                    {σ₁₂ : R →+* R₂} →
                      {σ₂₁ : R₂ →+* R} →
                        [inst_6 : RingHomInvPair σ₁₂ σ₂₁] →
                          [inst_7 : RingHomInvPair σ₂₁ σ₁₂] →
                            [Subsingleton M] → [Subsingleton M₂] → Unique (M ≃ₛₗ[σ₁₂] M₂)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- Multiplying each row by a fixed `v i` multiplies the determinant by
the product of the `v`s.  -/
Matrix.det_mul_row : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (v : n → R)
  (A : Matrix n n R), (Matrix.of fun i j => v j * A i j).det = (∏ i, v i) * A.det
-- Mathlib.RingTheory.MvPolynomial
MvPolynomial.instModule : {σ : Type u} → {K : Type v} → [inst : CommRing K] → Module K (MvPolynomial σ K)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.orElse_Option : ∀ {α : Type u_1} {x : Option α} {h : Unit → Option α}
  (Q : Std.Do.PostCond α (Std.Do.PostShape.except PUnit.{u_1 + 1} Std.Do.PostShape.pure)),
  ⦃(Std.Do.wp x).apply (Q.1, fun x => (Std.Do.wp (h ())).apply Q, Q.2.2)⦄ OrElse.orElse x h ⦃Q⦄
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.symm_bijective : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B]
  [inst_4 : SMul R A] [inst_5 : SMul R B] [inst_6 : Star A] [inst_7 : Star B], Function.Bijective StarAlgEquiv.symm
-- Mathlib.Analysis.RCLike.Basic
RCLike.conjCLE_coe : ∀ {K : Type u_1} [inst : RCLike K], ↑RCLike.conjCLE = ↑RCLike.conjAe
-- Std.Data.DTreeMap.Internal.Queries
/-- Returns the entry (key-value pair) for the key `k`, or `none` if such a key does not exist.  -/
Std.DTreeMap.Internal.Impl.getEntry? : {α : Type u} → {β : α → Type v} → [Ord α] → Std.DTreeMap.Internal.Impl α β → α → Option ((a : α) × β a)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
LinearIsometry.toContinuousLinearMap_rTensor : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f : E →ₗᵢ[𝕜] F),
  (LinearIsometry.rTensor G f).toContinuousLinearMap = ContinuousLinearMap.rTensor G f.toContinuousLinearMap
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.OptionT.orElse.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a))
  (h_2 : (x : Option α) → motive x),
  (match some a with
    | some a => h_1 a
    | x => h_2 x) =
    h_1 a
-- Mathlib.Analysis.Normed.Group.Quotient
_private.Mathlib.Analysis.Normed.Group.Quotient.0.QuotientAddGroup.add_norm_aux : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {S : AddSubgroup M} (x : M ⧸ S), {m | ↑m = x}.Nonempty
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- A morphism `X ⟶ Y` induces a functor `Under Y ⥤ Under X` in the obvious way.  -/
CategoryTheory.Under.map : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {X Y : T} → (X ⟶ Y) → CategoryTheory.Functor (CategoryTheory.Under Y) (CategoryTheory.Under X)
-- Mathlib.Analysis.LocallyConvex.AbsConvex
AbsConvex.empty : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜], AbsConvex 𝕜 ∅
-- Mathlib.MeasureTheory.OuterMeasure.Defs
/-- An outer measure is a countably subadditive monotone function that sends `∅` to `0`.  -/
MeasureTheory.OuterMeasure : Type u_2 → Type u_2
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.coe_range : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N), ↑f.range = Set.range ⇑f
-- Mathlib.Data.Ineq
Mathlib.Ineq.lt.sizeOf_spec : sizeOf Mathlib.Ineq.lt = 1
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsType₂.eq_1 : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N),
  SSet.prodStdSimplex.pairingCore.IsType₂ x =
    ∀ (d : ℕ) (hd : x.dim = d) (l : Fin (d + 1)), ¬SSet.prodStdSimplex.pairingCore.IsIndex x hd l
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.cotangentComplex_mk : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (P : Algebra.Extension R S)
  (x : ↥P.ker), P.cotangentComplex (Algebra.Extension.Cotangent.mk x) = 1 ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) ↑x
-- Mathlib.GroupTheory.CoprodI
_private.Mathlib.GroupTheory.CoprodI.0.Monoid.CoprodI.NeWord.toList.match_1.splitter : {ι : Type u_1} →
  {M : ι → Type u_2} →
    [inst : (i : ι) → Monoid (M i)] →
      (motive : (x x_1 : ι) → Monoid.CoprodI.NeWord M x x_1 → Sort u_3) →
        (x x_1 : ι) →
          (x_2 : Monoid.CoprodI.NeWord M x x_1) →
            ((i : ι) → (x : M i) → (a : x ≠ 1) → motive i i (Monoid.CoprodI.NeWord.singleton x a)) →
              ((x x_3 j k : ι) →
                  (w₁ : Monoid.CoprodI.NeWord M x j) →
                    (_hne : j ≠ k) → (w₂ : Monoid.CoprodI.NeWord M k x_3) → motive x x_3 (w₁.append _hne w₂)) →
                motive x x_1 x_2
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- An arrow of `S.pullback f` gives rise to an arrow of `S`.  -/
CategoryTheory.GrothendieckTopology.Cover.Arrow.base : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {J : CategoryTheory.GrothendieckTopology C} → {f : Y ⟶ X} → {S : J.Cover X} → (S.pullback f).Arrow → S.Arrow
-- Mathlib.GroupTheory.Order.Min
AddMonoid.minOrder_eq_top_iff : ∀ {G : Type u_1} [inst : AddCommGroup G], AddMonoid.minOrder G = ⊤ ↔ IsAddTorsionFree G
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.eqToEquivalence.congr_simp : ∀ {I : Type w₀} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {i j : I} (h : i = j),
  CategoryTheory.Pi.eqToEquivalence C h = CategoryTheory.Pi.eqToEquivalence C h
-- Mathlib.Analysis.InnerProductSpace.EuclideanDist
Euclidean.closedBall_eq_preimage : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : IsTopologicalAddGroup E]
  [inst_3 : T2Space E] [inst_4 : Module ℝ E] [inst_5 : ContinuousSMul ℝ E] [inst_6 : FiniteDimensional ℝ E] (x : E)
  (r : ℝ), Euclidean.closedBall x r = ⇑toEuclidean ⁻¹' Metric.closedBall (toEuclidean x) r
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {h_mem : k ∈ t₁ ∩ t₂}, (t₁ ∩ t₂).getKey k h_mem = t₁.getKey k ⋯
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.div_const : ∀ {G : Type u_2} {α : Type u_3} [inst : MeasurableSpace G] [inst_1 : Div G] {m : MeasurableSpace α} {f : α → G}
  {μ : MeasureTheory.Measure α} [MeasurableDiv G], AEMeasurable f μ → ∀ (c : G), AEMeasurable (fun x => f x / c) μ
-- Mathlib.Algebra.Polynomial.Div
Polynomial.mul_divByMonic_eq_iff_isRoot : ∀ {R : Type u} {a : R} [inst : CommRing R] {p : Polynomial R},
  (Polynomial.X - Polynomial.C a) * (p /ₘ (Polynomial.X - Polynomial.C a)) = p ↔ p.IsRoot a
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_castLE_Ico : ∀ {n m : ℕ} (a b : Fin n) (h : n ≤ m),
  Finset.image (Fin.castLE h) (Finset.Ico a b) = Finset.Ico (Fin.castLE h a) (Fin.castLE h b)
-- Init.Data.List.Basic
/-- Returns the index of the first element for which `p` returns `true`, or the length of the list if
there is no such element.

Examples:
* `[7, 6, 5, 8, 1, 2, 6].findIdx (· < 5) = 4`
* `[7, 6, 5, 8, 1, 2, 6].findIdx (· < 1) = 7`
 -/
List.findIdx : {α : Type u} → (α → Bool) → List α → ℕ
-- Mathlib.NumberTheory.Padics.MahlerBasis
PadicInt.norm_mahlerTerm : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : Module ℤ_[p] E]
  [inst_2 : IsBoundedSMul ℤ_[p] E] (a : E) (n : ℕ), ‖PadicInt.mahlerTerm a n‖ = ‖a‖
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.coe_symm_toEquiv : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] (e : A ≃ₗc[R] B), ⇑e.toEquiv.symm = ⇑e.symm
-- Mathlib.Topology.UnitInterval
Set.Icc.convexComb_one : ∀ {a b : ℝ} (x y : ↑(Set.Icc a b)), Set.Icc.convexComb x y 1 = y
-- Lean.Elab.InfoTree.Types
Lean.Elab.ElabInfo.mk.injEq : ∀ (elaborator : Lean.Name) (stx : Lean.Syntax) (elaborator_1 : Lean.Name) (stx_1 : Lean.Syntax),
  ({ elaborator := elaborator, stx := stx } = { elaborator := elaborator_1, stx := stx_1 }) =
    (elaborator = elaborator_1 ∧ stx = stx_1)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- A point is in the inf of two affine subspaces if and only if it is in both of them.  -/
AffineSubspace.mem_inf_iff : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (p : P) (s₁ s₂ : AffineSubspace k P), p ∈ s₁ ⊓ s₂ ↔ p ∈ s₁ ∧ p ∈ s₂
-- Mathlib.Data.Finset.Attach
/-- `attach s` takes the elements of `s` and forms a new set of elements of the subtype
`{x // x ∈ s}`.  -/
Finset.attach : {α : Type u_1} → (s : Finset α) → Finset ↥s
-- Mathlib.Order.Filter.Germ.Basic
/-- Given a germ `f : Germ l β` and a function `F : (α → β) → γ` sending eventually equal functions
to the same value, returns the value `F` takes on functions having germ `f` at `l`.  -/
Filter.Germ.liftOn : {α : Type u_1} →
  {β : Type u_2} →
    {l : Filter α} →
      {γ : Sort u_5} → l.Germ β → (F : (α → β) → γ) → Relator.LiftFun l.EventuallyEq (fun x1 x2 => x1 = x2) F F → γ
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.diff_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ m₃ m₄ : Std.HashMap α β} [EquivBEq α]
  [LawfulHashable α], m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁ \ m₂).Equiv (m₃ \ m₄)
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.mem_iSup_prop : ∀ {M : Type u_1} [inst : AddZeroClass M] {p : Prop} {S : p → AddSubmonoid M} {x : M},
  x ∈ ⨆ (h : p), S h ↔ x = 0 ∨ ∃ (h : p), x ∈ S h
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.smul_restrictScalars : ∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) (r : R) (M : ModuleCat S),
  ((ModuleCat.restrictScalars f).obj M).smul r = M.smul (f r)
-- Mathlib.Algebra.Ring.Parity
odd_add_one_self' : ∀ {α : Type u_2} [inst : Semiring α] {a : α}, Odd (a + (1 + a))
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.getGE?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getGE? k = t₂.getGE? k
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- The canonical morphism from `S.bind T` to `T`.  -/
CategoryTheory.GrothendieckTopology.Cover.bindToBase : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {X : C} → (S : J.Cover X) → (T : (I : S.Arrow) → J.Cover I.Y) → S.bind T ⟶ S
-- Init.Data.BitVec.Basic
/-- The bitvector of width `w` that has the smallest value when interpreted as an integer.  -/
BitVec.intMin : (w : ℕ) → BitVec w
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.tensorδ_tensorμ_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X₁ X₂ Y₁ Y₂ : C) {Z : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₁)
        (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ Y₂) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorδ X₁ X₂ Y₁ Y₂)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ X₁ X₂ Y₁ Y₂) h) =
    h
-- Init.Data.Float.Model.Unpacked.Basic
/-- Signed infinity.  -/
Float.Model.UnpackedFloat.infinity : Float.Model.UnpackedFloat.Sign → Float.Model.UnpackedFloat
-- Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
CategoryTheory.Limits.SequentialProduct.cone_π_app_comp_Pi_π_neg_assoc : ∀ {C : Type u_1} {M N : ℕ → C} [inst : CategoryTheory.Category.{v_1, u_1} C] (f : (n : ℕ) → M n ⟶ N n)
  [inst_1 : CategoryTheory.Limits.HasCountableProducts C] (m n : ℕ) (h : ¬n < m) {Z : C}
  (h_1 : (if x : n < m then M n else N n) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.SequentialProduct.cone f).π.app (Opposite.op m))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.Pi.π (fun m_1 => if x : m_1 < m then M m_1 else N m_1) n) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π M n)
      (CategoryTheory.CategoryStruct.comp (f n) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h_1))
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.restrict_finitary : ∀ {α : Type u_1} {M : Matroid α} [M.Finitary] (R : Set α), (M.restrict R).Finitary
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.mk_neg : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Neg G] [inst_2 : ContinuousNeg G] (x : G),
  SeparationQuotient.mk (-x) = -SeparationQuotient.mk x
-- Mathlib.Analysis.Convex.AmpleSet
/-- Images of ample sets under continuous affine equivalences are ample.  -/
AmpleSet.image : ∀ {F : Type u_1} [inst : AddCommGroup F] [inst_1 : Module ℝ F] [inst_2 : TopologicalSpace F] {E : Type u_2}
  [inst_3 : AddCommGroup E] [inst_4 : Module ℝ E] [inst_5 : TopologicalSpace E] {s : Set E},
  AmpleSet s → ∀ (L : E ≃ᴬ[ℝ] F), AmpleSet (⇑L '' s)
-- Mathlib.GroupTheory.Submonoid.Center
Submonoid.mem_center_iff : ∀ {M : Type u_1} [inst : Monoid M] {z : M}, z ∈ Submonoid.center M ↔ ∀ (g : M), g * z = z * g
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instSub.eq_1 : ∀ {α : Type u_1} [inst : Sub α], OrderDual.instSub = inst
-- Mathlib.Algebra.Algebra.Opposite
AlgEquiv.op_symm_apply_apply : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) (a : A),
  (AlgEquiv.op.symm f) a = MulOpposite.unop (f (MulOpposite.op a))
-- Init.Data.UInt.Lemmas
instLawfulCommIdentityUInt64HMulOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 * x2) 1
-- Lean.Elab.Term.TermElabM
/-- Noncomputable sections automatically add the `noncomputable` modifier to any declaration we cannot generate code for.  -/
Lean.Elab.Term.Context.isNoncomputableSection : Lean.Elab.Term.Context → Bool