mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Internal.List.Associative
Std.Internal.List.perm_filter_not_contains_map_fst_of_perm : ∀ {α : Type u} {β : α → Type v} {l₁ l₂ l₃ : List ((a : α) × β a)} [inst : BEq α] [EquivBEq α],
  l₂.Perm l₃ →
    Std.Internal.List.DistinctKeys l₁ →
      (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁).Perm
        (List.filter (fun p => !(List.map Sigma.fst l₃).contains p.fst) l₁)
-- Lean.Server.References
/-- Yields all definitions matching the given `filter`.  -/
Lean.Server.References.definitionsMatching : {α : Type} →
  Lean.Server.References →
    (Lean.Name → Option α) →
      optParam (Option IO.CancelToken) none → BaseIO (Array (Lean.Server.References.MatchedDefinition α))
-- Mathlib.GroupTheory.ArchimedeanDensely
/-- If an element of a linearly ordered archimedean additive group is the least positive element,
then the whole group is isomorphic (and order-isomorphic) to the integers.  -/
LinearOrderedAddCommGroup.int_orderAddMonoidIso_of_isLeast_pos : {G : Type u_2} →
  [inst : AddCommGroup G] →
    [inst_1 : LinearOrder G] → [IsOrderedAddMonoid G] → [Archimedean G] → {x : G} → IsLeast {y | 0 < y} x → G ≃+o ℤ
-- Mathlib.LinearAlgebra.FreeModule.ModN
/-- The universal property of `ModN G n` in terms of `ZMod n`-modules: `ZMod n`-linear maps from
`ModN G n` are the same as monoid homomorphisms from `G` whose values are `n`-torsion.  -/
ModN.liftEquiv' : {G : Type u_1} →
  {H : Type u_2} →
    [inst : AddCommGroup G] →
      {n : ℕ} →
        [inst_1 : AddCommGroup H] →
          [inst_2 : Module (ZMod n) H] → (ModN G n →ₗ[ZMod n] H) ≃ { φ // ∀ (g : G), n • φ g = 0 }
-- Lean.Data.JsonRpc
Lean.JsonRpc.Message.request.injEq : ∀ (id : Lean.JsonRpc.RequestID) (method : String) (params? : Option Lean.Json.Structured)
  (id_1 : Lean.JsonRpc.RequestID) (method_1 : String) (params?_1 : Option Lean.Json.Structured),
  (Lean.JsonRpc.Message.request id method params? = Lean.JsonRpc.Message.request id_1 method_1 params?_1) =
    (id = id_1 ∧ method = method_1 ∧ params? = params?_1)
-- Aesop.RuleSet
Aesop.instInhabitedLocalRuleSet : Inhabited Aesop.LocalRuleSet
-- Mathlib.Computability.Partrec
Partrec.of_eq_tot : ∀ {α : Type u_1} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α →. σ} {g : α → σ},
  Partrec f → (∀ (n : α), g n ∈ f n) → Computable g
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.unitAuxAux_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A)
  (X : Cᵒᵖ),
  (CategoryTheory.OverPresheafAux.unitAuxAux η).hom.app X =
    TypeCat.ofHom (CategoryTheory.OverPresheafAux.unitForward η (Opposite.unop X))
-- Mathlib.RingTheory.Invariant.Basic
IsFractionRing.stabilizerHom.congr_simp : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (G : Type u_3)
  [inst_3 : Group G] [inst_4 : MulSemiringAction G B] [inst_5 : SMulCommClass G A B] (P : Ideal A) (Q : Ideal B)
  [inst_6 : Q.LiesOver P] (K : Type u_4) (L : Type u_5) [inst_7 : Field K] [inst_8 : Field L]
  [inst_9 : Algebra (A ⧸ P) K] [inst_10 : Algebra (B ⧸ Q) L] [inst_11 : Algebra (A ⧸ P) L]
  [inst_12 : IsScalarTower (A ⧸ P) (B ⧸ Q) L] [inst_13 : Algebra K L] [inst_14 : IsScalarTower (A ⧸ P) K L]
  [inst_15 : IsFractionRing (A ⧸ P) K] [inst_16 : IsFractionRing (B ⧸ Q) L],
  IsFractionRing.stabilizerHom G P Q K L = IsFractionRing.stabilizerHom G P Q K L
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.restr_symm_trans : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {s : Set X} {e' : OpenPartialHomeomorph X Y},
  IsOpen s → IsOpen (↑e '' s) → s ⊆ e.source → (e.restr s).symm.trans e' ≈ (e.symm.trans e').restr (↑e '' s)
-- Mathlib.Analysis.Normed.Group.Uniform
LipschitzWith.norm_neg_add_le_of_le : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F] {a b : E} {r : ℝ}
  {f : E → F} {C : NNReal}, LipschitzWith C f → ‖-a + b‖ ≤ r → ‖-f a + f b‖ ≤ ↑C * r
-- Mathlib.Topology.UnitInterval
Set.Icc.monotone_addNSMul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] {a b : α} (h : a ≤ b) {δ : α},
  0 ≤ δ → Monotone (Set.Icc.addNSMul h δ)
-- Mathlib.Analysis.Calculus.Implicit
/-- Derivative of the left function  -/
ImplicitFunctionData.leftDeriv : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          [inst_3 : CompleteSpace E] →
            {F : Type u_3} →
              [inst_4 : NormedAddCommGroup F] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [inst_6 : CompleteSpace F] →
                    {G : Type u_4} →
                      [inst_7 : NormedAddCommGroup G] →
                        [inst_8 : NormedSpace 𝕜 G] →
                          [inst_9 : CompleteSpace G] → ImplicitFunctionData 𝕜 E F G → E →L[𝕜] F
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.C_comp : ∀ {R : Type u} {a : R} [inst : Semiring R] {p : Polynomial R}, (Polynomial.C a).comp p = Polynomial.C a
-- Mathlib.AlgebraicGeometry.Restrict
/-- The functor taking open subsets of `X` to open subschemes of `X`.  -/
AlgebraicGeometry.Scheme.restrictFunctor : (X : AlgebraicGeometry.Scheme) → CategoryTheory.Functor X.Opens (CategoryTheory.Over X)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_insertIfNew : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k a : α}
  [inst_1 : Inhabited (β a)] {v : β k},
  (m.insertIfNew k v).get! a = if h : (k == a) = true ∧ k ∉ m then cast ⋯ v else m.get! a
-- Mathlib.Algebra.Homology.Single
/-- The natural isomorphism `single V c j ⋙ eval V c j ≅ 𝟭 V`.  -/
HomologicalComplex.singleCompEvalIsoSelf : (V : Type u) →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject V] →
        {ι : Type u_1} →
          [inst_3 : DecidableEq ι] →
            (c : ComplexShape ι) →
              (j : ι) →
                (HomologicalComplex.single V c j).comp (HomologicalComplex.eval V c j) ≅ CategoryTheory.Functor.id V
-- Mathlib.Data.Set.Insert
Set.set_compr_eq_eq_singleton : ∀ {α : Type u_1} {a : α}, {b | b = a} = {a}
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Affine.Simplex.faceOppositeCentroid.congr_simp : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s s_1 : Affine.Simplex k P n),
  s = s_1 → ∀ (i i_1 : Fin (n + 1)), i = i_1 → s.faceOppositeCentroid i = s_1.faceOppositeCentroid i_1
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn_roc : ∀ {α β : Type u} {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  [inst_2 : LE α] [inst_3 : DecidableLE α] [inst_4 : LT α] [inst_5 : Std.PRange.UpwardEnumerable α]
  [inst_6 : Std.Rxc.IsAlwaysFinite α] [inst_7 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_8 : Std.PRange.LawfulUpwardEnumerableLE α] [inst_9 : Std.PRange.LawfulUpwardEnumerableLT α] {xs : Std.Roc α}
  {init : β} {f : α → β → m (ForInStep β)} (inv : Std.Do.Invariant xs.toList β ps),
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f cur b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
          | ForInStep.done b' => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'),
          inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := xs.toList, property := ⋯ }, init)⦄
      forIn xs init f ⦃(fun b => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b), inv.2)⦄
-- Init.Data.List.MinMax
List.get_max? : ∀ {α : Type u_1} [inst : Max α] {l : List α} {h : l.max?.isSome = true}, l.max?.get h = l.max ⋯
-- Init.Data.List.Nat.Range
List.sum_range' : ∀ {start n step : ℕ}, (List.range' start n step).sum = n * start + n * (n - 1) * step / 2
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.instPartialOrderSubobject : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → (X : C) → PartialOrder (CategoryTheory.Subobject X)
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than or equal to the
given key, returning `none` if no such pair exists.
 -/
Std.ExtDTreeMap.getEntryLE? : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → α → Option ((a : α) × β a)
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.coeff_subst_finite : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S},
  MvPowerSeries.HasSubst a →
    ∀ (f : MvPowerSeries σ R) (e : τ →₀ ℕ),
      Function.HasFiniteSupport fun d => (MvPowerSeries.coeff d) f • (MvPowerSeries.coeff e) (d.prod fun s e => a s ^ e)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
_private.Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C),
  (CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor✝ t n).obj X =
    CategoryTheory.Triangulated.TStructure.TruncAux.triangle✝ t n X
-- Mathlib.Topology.Neighborhoods
mem_of_mem_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X}, s ∈ nhds x → x ∈ s
-- Std.Http.Protocol.H1
/-- Marks writer message as complete and continues the writer state machine to apply
post-completion transitions.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.completeWriterMessage : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerMap_assoc₁ : ∀ {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12}
  {q : Type u_13} {r : Type u_14} {δ : Type u_19} {ξ : Type u_20} {ω : Type u_21} (f : α → β → γ) (g : γ → δ → ω)
  (f' : α → ξ → ω) (g' : β → δ → ξ) (A : Matrix l m α) (B : Matrix n p β) (D : Matrix q r δ),
  (∀ (a : α) (b : β) (d : δ), g (f a b) d = f' a (g' b d)) →
    (Matrix.reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r))
        (Matrix.kroneckerMap g (Matrix.kroneckerMap f A B) D) =
      Matrix.kroneckerMap f' A (Matrix.kroneckerMap g' B D)
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inr_desc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G K : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (α : G ⟶ K) (hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inr φ)
      (HomologicalComplex.homotopyCofiber.desc φ α hα) =
    α
-- Mathlib.Tactic.Determinant.Bird.Cert
Mathlib.Tactic.Determinant.CertCache.mk.injEq : ∀ {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)}
  (entryCache : Std.HashMap (ℕ × ℕ) (Mathlib.Tactic.Determinant.Cert rα))
  (iterStepEntryCache : Std.HashMap (ℕ × ℕ × ℕ) (Mathlib.Tactic.Determinant.Cert rα))
  (diagCache entryCache_1 : Std.HashMap (ℕ × ℕ) (Mathlib.Tactic.Determinant.Cert rα))
  (iterStepEntryCache_1 : Std.HashMap (ℕ × ℕ × ℕ) (Mathlib.Tactic.Determinant.Cert rα))
  (diagCache_1 : Std.HashMap (ℕ × ℕ) (Mathlib.Tactic.Determinant.Cert rα)),
  ({ entryCache := entryCache, iterStepEntryCache := iterStepEntryCache, diagCache := diagCache } =
      { entryCache := entryCache_1, iterStepEntryCache := iterStepEntryCache_1, diagCache := diagCache_1 }) =
    (entryCache = entryCache_1 ∧ iterStepEntryCache = iterStepEntryCache_1 ∧ diagCache = diagCache_1)
-- Mathlib.NumberTheory.LucasLehmer
/-- `ω` as an element of the group of units.  -/
LucasLehmer.ωUnit : (p : ℕ) → (LucasLehmer.X ↑(LucasLehmer.q p))ˣ
-- Mathlib.Algebra.Module.Projective
Module.Projective.of_equiv' : ∀ {R : Type u_1} [inst : Semiring R] {P : Type u_2} [inst_1 : AddCommMonoid P] [inst_2 : Module R P] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [Module.Projective R M] (e : M ≃ₗ[R] P), Module.Projective R P
-- Lean.Elab.PreDefinition.FixedParams
_private.Lean.Elab.PreDefinition.FixedParams.0.Lean.Elab.FixedParamPerm.instantiateLambda.go : Array Lean.Expr → List (Option ℕ) → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.NumberTheory.MaricaSchoenheim
/-- The special case of Graham's conjecture where all numbers are squarefree.  -/
Nat.grahamConjecture_of_squarefree : ∀ {n : ℕ} (f : ℕ → ℕ), (∀ k < n, Squarefree (f k)) → n.GrahamConjecture f
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
HomotopyCategory.Plus.instEssSurjInjectiveObjectPlusCompMapHomotopyCategoryPlusιQh : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.EnoughInjectives C] [inst_3 : HasDerivedCategory C],
  ((CategoryTheory.InjectiveObject.ι C).mapHomotopyCategoryPlus.comp DerivedCategory.Plus.Qh).EssSurj
-- Mathlib.Order.Minimal
Set.maximal_iff_forall_insert : ∀ {α : Type u_2} {P : Set α → Prop} {s : Set α},
  (∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s) → (Maximal P s ↔ P s ∧ ∀ x ∉ s, ¬P (insert x s))
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.whisker_assoc_bimod : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C]
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_4 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  {W X Y Z : CategoryTheory.Mon C} (M : Bimod W X) {N N' : Bimod X Y} (f : N ⟶ N') (P : Bimod Y Z),
  Bimod.whiskerRight (M.whiskerLeft f) P =
    CategoryTheory.CategoryStruct.comp (M.associatorBimod N P).hom
      (CategoryTheory.CategoryStruct.comp (M.whiskerLeft (Bimod.whiskerRight f P)) (M.associatorBimod N' P).inv)
-- Mathlib.Algebra.CharP.Frobenius
RingHom.iterate_map_frobenius : ∀ {R : Type u_1} [inst : CommSemiring R] (x : R) (f : R →+* R) (p : ℕ) [inst_1 : ExpChar R p] (n : ℕ),
  (⇑f)^[n] ((frobenius R p) x) = (frobenius R p) ((⇑f)^[n] x)
-- Mathlib.RingTheory.Algebraic.Pi
/-- This is not an instance as it forms a diamond with `Pi.instSMul`.

See the `instance_diamonds` test for details.  -/
Polynomial.hasSMulPi' : (R : Type u_1) →
  (S : Type u_2) →
    (T : Type u_3) →
      [inst : CommSemiring R] → [inst_1 : Semiring S] → [Algebra R S] → [SMul S T] → SMul (Polynomial R) (S → T)
-- Mathlib.Algebra.Module.Submodule.Range
/-- The range of a linear map `f : M → M₂` is a submodule of `M₂`.
See Note [range copy pattern].  -/
LinearMap.range : {R : Type u_1} →
  {R₂ : Type u_2} →
    {M : Type u_5} →
      {M₂ : Type u_6} →
        [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₂} → [RingHomSurjective τ₁₂] → (M →ₛₗ[τ₁₂] M₂) → Submodule R₂ M₂
-- Mathlib.Algebra.CharP.Basic
CharP.intCast_eq_intCast : ∀ (R : Type u_1) [inst : AddGroupWithOne R] (p : ℕ) [CharP R p] {a b : ℤ}, ↑a = ↑b ↔ a ≡ b [ZMOD ↑p]
-- Lean.Elab.Tactic.Omega.Core
/-- The justification for the constraint constructed using "balanced mod" while
eliminating an equality.
 -/
Lean.Elab.Tactic.Omega.Justification.bmod : (m : ℕ) →
  (r : ℤ) →
    (i : ℕ) →
      {x : Lean.Omega.Coeffs} →
        Lean.Elab.Tactic.Omega.Justification (Lean.Omega.Constraint.exact r) x →
          Lean.Elab.Tactic.Omega.Justification (Lean.Omega.Constraint.exact (r.bmod m)) (Lean.Omega.bmod_coeffs m i x)
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_eq_closure : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M},
  (Submodule.span R s).toAddSubmonoid = AddSubmonoid.closure (Set.univ • s)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_filter_of_getKey?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Bool} {k k' : α},
  m.WF →
    m.getKey? k = some k' →
      Std.DHashMap.Raw.Const.get? (Std.DHashMap.Raw.filter f m) k =
        Option.filter (fun x => f k' x) (Std.DHashMap.Raw.Const.get? m k)
-- Mathlib.RingTheory.Int.Basic
Int.isCoprime_two_left : ∀ {m : ℤ}, IsCoprime 2 m ↔ Odd m
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.coloops_indep : ∀ {α : Type u_1} (M : Matroid α), M.Indep M.coloops
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.filterMap.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.Data.TypeVec
TypeVec.prod.snd.eq_2 : ∀ (n : ℕ) (x_4 x_5 : TypeVec.{u} n.succ), TypeVec.prod.snd Fin2.fz = Prod.snd
-- Mathlib.LinearAlgebra.Vandermonde
/-- A square matrix with rows all having the form `[b^(n-1), a * b^(n-2), ..., a ^ (n-1)]`  -/
Matrix.projVandermonde : {R : Type u_1} → [CommRing R] → {n : ℕ} → (Fin n → R) → (Fin n → R) → Matrix (Fin n) (Fin n) R
-- Mathlib.Data.QPF.Multivariate.Constructions.Comp
MvQPF.Comp.get_map : ∀ {n m : ℕ} {F : TypeVec.{u} n → Type u_1} {G : Fin2 n → TypeVec.{u} m → Type u} {α β : TypeVec.{u} m} (f : α.Arrow β)
  [inst : MvFunctor F] [inst_1 : (i : Fin2 n) → MvFunctor (G i)] (x : MvQPF.Comp F G α),
  (MvFunctor.map f x).get = MvFunctor.map (fun i x => MvFunctor.map f x) x.get
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.ext : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] {f g : M₁ →SL[σ₁₂] M₂},
  (∀ (x : M₁), f x = g x) → f = g
-- Mathlib.Order.WithBot
WithBot.map_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : β → γ) (g : α → β) (a : WithBot α),
  WithBot.map h (WithBot.map g a) = WithBot.map (h ∘ g) a
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_singleton_eq_span_singleton : ∀ {α : Type u} [inst : CommSemiring α] [IsDomain α] {x y : α}, Ideal.span {x} = Ideal.span {y} ↔ Associated x y
-- Init.Data.Float.Model.Unpacked.Basic
/-- Not a number. There is no payload attached to a NaN in this format.  -/
Float.Model.UnpackedFloat.notANumber : Float.Model.UnpackedFloat
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
/-- Given two refinement morphisms `f, g : E ⟶ F`, this is a (pre-)`1`-hypercover `W` that
admits a morphism `h : W ⟶ E` such that `h ≫ f` and `h ≫ g` are homotopic. Hence
they become equal after quotienting out by homotopy.
This is a `1`-hypercover, if `E` and `F` are (see `OneHypercover.cylinder`).  -/
CategoryTheory.PreOneHypercover.cylinder : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreOneHypercover S} →
        {F : CategoryTheory.PreOneHypercover S} →
          [CategoryTheory.Limits.HasPullbacks C] → E.Hom F → E.Hom F → CategoryTheory.PreOneHypercover S
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.Cover.locallyDirectedPullbackCover : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {X : AlgebraicGeometry.Scheme} →
    [inst : P.IsStableUnderBaseChange] →
      (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) →
        [inst_1 : CategoryTheory.Category.{v_2, u_1} 𝒰.I₀] →
          [𝒰.LocallyDirected] →
            {Y : AlgebraicGeometry.Scheme} →
              (f : Y ⟶ X) →
                AlgebraicGeometry.Scheme.Cover.LocallyDirected (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰)
-- Batteries.Tactic.PrintPrefix
/-- `matchName opts pre cinfo` returns true if the search options should include the constant.
 -/
_private.Batteries.Tactic.PrintPrefix.0.Batteries.Tactic.matchName : Batteries.Tactic.PrintPrefixConfig → Lean.Name → Lean.ConstantInfo → Lean.MetaM Bool
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the smallest key that is greater than the given key,
returning `none` if no such key exists.
 -/
Std.ExtDTreeMap.getKeyGT? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → α → Option α
-- Mathlib.Topology.ContinuousMap.Compact
/-- When `α` is compact, the bounded continuous maps `α →ᵇ β` are
equivalent to `C(α, β)`.
 -/
ContinuousMap.equivBoundedOfCompact : (α : Type u_1) →
  (β : Type u_2) →
    [inst : TopologicalSpace α] →
      [CompactSpace α] → [inst_2 : PseudoMetricSpace β] → C(α, β) ≃ BoundedContinuousFunction α β
-- Init.Data.Range.Polymorphic.UInt
UInt16.instHasSize : Std.Rxc.HasSize UInt16
-- Mathlib.NumberTheory.FactorisationProperties
Nat.Prime.not_weird : ∀ {n : ℕ}, Nat.Prime n → ¬n.Weird
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEmbedding.of_measurable_inverse_on_range : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β}
  {g : ↑(Set.range f) → α},
  Measurable f →
    MeasurableSet (Set.range f) →
      Measurable g → Function.LeftInverse g (Set.rangeFactorization f) → MeasurableEmbedding f
-- Mathlib.FieldTheory.Extension
IntermediateField.Lifts.union.congr_simp : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] (c c_1 : Set (IntermediateField.Lifts F E K)) (e_c : c = c_1)
  (hc : IsChain (fun x1 x2 => x1 ≤ x2) c), IntermediateField.Lifts.union c hc = IntermediateField.Lifts.union c_1 ⋯
-- Mathlib.NumberTheory.Cyclotomic.Basic
IsCyclotomicExtension.mem_of_pow_eq_one : ∀ (S : Set ℕ) {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [IsDomain B]
  (C : Subalgebra A B) [h : IsCyclotomicExtension S A ↥C] {m : ℕ} {ζ : B}, m ∈ S → m ≠ 0 → ζ ^ m = 1 → ζ ∈ C
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
/-- Restrictions of matroids with cardinal rank functions have cardinal rank functions.  -/
Matroid.invariantCardinalRank_restrict : ∀ {α : Type u} {M : Matroid α} {X : Set α} [M.InvariantCardinalRank], (M.restrict X).InvariantCardinalRank
-- Mathlib.Order.Ideal
Order.Ideal.principal_toLowerSet : ∀ {P : Type u_1} [inst : Preorder P] (p : P), (Order.Ideal.principal p).toLowerSet = LowerSet.Iic p
-- Lean.Parser.Types
/-- Returns the character at position `p` of the input string. Returns `(default : Char)`, which is
`'A'`, if `p` is not a valid position.

Requires evidence, `h`, that `p` is within bounds instead of performing a run-time bounds check as
in `InputContext.get`.

A typical pattern combines `get'` with a dependent `if`-expression to avoid the overhead of an
additional bounds check. For example:
```
def getInBounds? (s : String) (p : String.Pos) : Option Char :=
  if h : s.atEnd p then none else some (s.get' p h)
```
Even with evidence of `¬ s.atEnd p`, `p` may be invalid if a byte index points into the middle of a
multi-byte UTF-8 character.
 -/
Lean.Parser.InputContext.get' : (c : Lean.Parser.InputContext) → (p : String.Pos.Raw) → ¬c.atEnd p = true → Char