mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.isColoop_iff_forall_mem_compl_isCircuit : ∀ {α : Type u_1} {M : Matroid α} {e : α} [M✶.RankPos], M.IsColoop e ↔ ∀ (C : Set α), M.IsCircuit C → e ∈ M.E \ C
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.whitespace : Lean.ParseImports.Parser
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsSymm.eq_iff : ∀ {R : Type u_1} {M : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {I : R →+* R}
  {B : M →ₛₗ[I] M →ₗ[R] R}, B.IsSymm → ∀ {x y : M}, (B x) y = 0 ↔ (B y) x = 0
-- Mathlib.Tactic.Algebra.Basic
/-- Collect all scalar rings from scalar multiplications and `algebraMap` applications in the
expression.  -/
Mathlib.Tactic.Algebra.collectScalarRings : Lean.Expr → Lean.MetaM (List Lean.Expr)
-- Lean.LocalContext
Lean.LocalContext.isSubPrefixOfAux : Lean.PArray (Option Lean.LocalDecl) → Lean.PArray (Option Lean.LocalDecl) → Array Lean.Expr → ℕ → ℕ → Bool
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- If `u` is a uniform structure on `β` and `f : γ → β`, then
`𝒱(α, γ, 𝔖, comap f u) = comap (fun g ↦ f ∘ g) 𝒱(α, γ, 𝔖, u₁)`.  -/
UniformOnFun.comap_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace β] {𝔖 : Set (Set α)} {f : γ → β},
  UniformOnFun.uniformSpace α γ 𝔖 = UniformSpace.comap (fun x => f ∘ x) (UniformOnFun.uniformSpace α β 𝔖)
-- Mathlib.Order.Cover
wcovBy_congr_right : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → (c ⩿ a ↔ c ⩿ b)
-- Mathlib.Data.Finset.Filter
Finset.filter_inj' : ∀ {α : Type u_1} {p q : α → Prop} [inst : DecidablePred p] [inst_1 : DecidablePred q] {s : Finset α},
  Finset.filter p s = Finset.filter q s ↔ ∀ ⦃a : α⦄, a ∈ s → (p a ↔ q a)
-- Init.System.IO
/-- The `Task` has finished running and its result is available. Calling `Task.get` or `IO.wait` on
the task will not block.
 -/
IO.TaskState.finished : IO.TaskState
-- Mathlib.Topology.Algebra.UniformConvergence
instAddCommMonoidUniformOnFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : AddCommMonoid β],
  instAddCommMonoidUniformOnFun = { toAddMonoid := instAddMonoidUniformOnFun, add_comm := ⋯ }
-- Init.Data.Ord.Basic
Ordering.isNe_lt : Ordering.lt.isNe = true
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- For any `σ : X ⟶ Y` between `n + 1`-truncated `StrictSegal` simplicial sets,
`spineToSimplex` commutes with `Path.map`.  -/
SSet.Truncated.StrictSegal.spineToSimplex_map : ∀ {n : ℕ} {X Y : SSet.Truncated (n + 1)} (sx : X.StrictSegal) (sy : Y.StrictSegal) (m : ℕ) (h : m ≤ n)
  (f : X.Path (m + 1)) (σ : X ⟶ Y),
  sy.spineToSimplex (m + 1) ⋯ (f.map σ) =
    (CategoryTheory.ConcreteCategory.hom (σ.app (Opposite.op { obj := { len := m + 1 }, property := ⋯ })))
      (sx.spineToSimplex (m + 1) ⋯ f)
-- Mathlib.CategoryTheory.Enriched.Basic
/-- The composition `V`-morphism for a `V`-enriched category.
 -/
CategoryTheory.eComp : (V : Type v) →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₁} →
        [inst_2 : CategoryTheory.EnrichedCategory V C] →
          (X Y Z : C) → CategoryTheory.MonoidalCategoryStruct.tensorObj (X ⟶[V] Y) (Y ⟶[V] Z) ⟶ X ⟶[V] Z
-- Init.Data.Nat.Lemmas
Nat.lt_log2_self : ∀ {n : ℕ}, n < 2 ^ (n.log2 + 1)
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.ofDiv.eq_1 : ∀ {G : Type u_1} [inst : Group G] (s : Set G) (hsn : s.Nonempty) (hs : ∀ x ∈ s, ∀ y ∈ s, x * y⁻¹ ∈ s),
  Subgroup.ofDiv s hsn hs = { carrier := s, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.mk.inj : ∀ {R : Type u} {A : Type v} {inst : CommSemiring R} {inst_1 : Semiring A} {inst_2 : Algebra R A}
  {toSubsemiring : Subsemiring A} {algebraMap_mem' : ∀ (r : R), (algebraMap R A) r ∈ toSubsemiring.carrier}
  {toSubsemiring_1 : Subsemiring A} {algebraMap_mem'_1 : ∀ (r : R), (algebraMap R A) r ∈ toSubsemiring_1.carrier},
  { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' } =
      { toSubsemiring := toSubsemiring_1, algebraMap_mem' := algebraMap_mem'_1 } →
    toSubsemiring = toSubsemiring_1
-- Init.Grind.AC
Lean.Grind.AC.diseq_simp_lhs_ac : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op}
  (c lhs₁ rhs₁ lhs₂ rhs₂ lhs₂' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.simp_ac_cert c lhs₁ rhs₁ lhs₂ lhs₂' = true →
    Lean.Grind.AC.Seq.denote ctx lhs₁ = Lean.Grind.AC.Seq.denote ctx rhs₁ →
      Lean.Grind.AC.Seq.denote ctx lhs₂ ≠ Lean.Grind.AC.Seq.denote ctx rhs₂ →
        Lean.Grind.AC.Seq.denote ctx lhs₂' ≠ Lean.Grind.AC.Seq.denote ctx rhs₂
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roc_succ_right_eq_cons_map : ∀ {m n : ℕ}, m ≤ n → (m<...=n + 1).toList = (m + 1) :: List.map (fun x => x + 1) (m<...=n).toList
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_eq_get!_getKey? : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {a : α}, m.getKey! a = (m.getKey? a).get!
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.div.eq_1 : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.div = { div := fun a b => ⟨↑a / ↑b, ⋯⟩ }
-- Mathlib.NumberTheory.RamificationInertia.Inertia
/-- **Alias** of `Ideal.inertiaDeg'_bot`. -/
Ideal.inertiaDeg_bot : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (P : Ideal S)
  [Nontrivial R] [IsDomain S] [Algebra.IsIntegral R S] [hP : P.LiesOver ⊥], ⊥.inertiaDeg' P = Module.finrank R S
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey_erase : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h : m.WF) {k a : α} {h' : a ∈ m.erase k}, (m.erase k).getKey a h' = m.getKey a ⋯
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.npow_def : ∀ {X : Type u_1} [inst : TopologicalSpace X] (k : ℕ) (m : X ≃ₜ X), NPow.npow k m = npowRecAuto k m
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- A terminal object in `A` gives rise to a terminal object in `Sheaf J`  -/
CategoryTheory.Sheaf.terminal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {A : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
          {X : A} → CategoryTheory.Limits.IsTerminal X → CategoryTheory.Sheaf J A
-- Batteries.Data.Vector.Lemmas
Vector.scanl_push : ∀ {β : Type u_1} {α : Type u_2} {n : ℕ} {init : β} {f : β → α → β} {as : Vector α n} {a : α},
  Vector.scanl f init (as.push a) = (Vector.scanl f init as).push (f (Vector.foldl f init as) a)
-- Lean.Elab.App
Lean.Elab.Term.ElabElimInfo.mk.inj : ∀ {elimExpr elimType : Lean.Expr} {motivePos : ℕ} {majorsPos : Array ℕ} {elimExpr_1 elimType_1 : Lean.Expr}
  {motivePos_1 : ℕ} {majorsPos_1 : Array ℕ},
  { elimExpr := elimExpr, elimType := elimType, motivePos := motivePos, majorsPos := majorsPos } =
      { elimExpr := elimExpr_1, elimType := elimType_1, motivePos := motivePos_1, majorsPos := majorsPos_1 } →
    elimExpr = elimExpr_1 ∧ elimType = elimType_1 ∧ motivePos = motivePos_1 ∧ majorsPos = majorsPos_1
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.eq_rnDeriv₀ : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite ν]
  {s : MeasureTheory.Measure α} {f : α → ENNReal},
  AEMeasurable f ν → s.MutuallySingular ν → μ = s + ν.withDensity f → f =ᵐ[ν] μ.rnDeriv ν
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
InnerProductSpace.gramSchmidtOrthonormalBasis_inv_triangular : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι]
  [inst_6 : Fintype ι] [inst_7 : FiniteDimensional 𝕜 E] (h : Module.finrank 𝕜 E = Fintype.card ι) (f : ι → E) {i j : ι},
  i < j → inner 𝕜 ((InnerProductSpace.gramSchmidtOrthonormalBasis h f) j) (f i) = 0
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_surjective_eq_arrow_of_le : ∀ {α β : Type u} [Infinite α],
  Cardinal.mk β ≤ Cardinal.mk α → Cardinal.mk ↑{f | Function.Surjective f} = Cardinal.mk (α → β)
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreesLE_add : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (s t : Multiset σ),
  MvPolynomial.degreesLE R σ (s + t) = MvPolynomial.degreesLE R σ s * MvPolynomial.degreesLE R σ t
-- Mathlib.Logic.Basic
em' : ∀ (p : Prop), ¬p ∨ p
-- Init.Data.BitVec.Basic
BitVec.instGetElemNatBoolLt : {w : ℕ} → GetElem (BitVec w) ℕ Bool fun x i => i < w
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.addCommutator_comm : ∀ {G : Type u_1} [inst : AddGroup G] (H₁ H₂ : AddSubgroup G), ⁅H₁, H₂⁆ = ⁅H₂, H₁⁆
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.addEquiv_apply : ∀ {𝕜₁ : 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]
  (self : E →SWOT[σ] F), ContinuousLinearMapWOT.addEquiv self = self.toCLM
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.sub_eq_add_neg : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a b : Lean.Grind.Ring.OfSemiring.Q α),
  Lean.Grind.Ring.OfSemiring.sub a b = Lean.Grind.Ring.OfSemiring.add a (Lean.Grind.Ring.OfSemiring.neg b)
-- Mathlib.RingTheory.DedekindDomain.Different
differentialIdeal_le_iff : ∀ {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [inst_11 : IsDomain A]
  [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L]
  [IsIntegrallyClosed A] [inst_17 : IsDedekindDomain B] [inst_18 : Module.IsTorsionFree A B]
  [inst_19 : IsFractionRing B L] {I : Ideal B},
  I ≠ ⊥ → (differentIdeal A B ≤ I ↔ Submodule.map (↑A (Algebra.trace K L)) (Submodule.restrictScalars A ↑(↑I)⁻¹) ≤ 1)
-- Mathlib.Data.Nat.Factorial.Basic
/-- `n.ascFactorial k = (n + k - 1)! / (n - 1)!` for `n > 0` but without ℕ-division. See
`Nat.ascFactorial_eq_div` for the version with ℕ-division. Consider using
`factorial_mul_ascFactorial` to avoid complications of ℕ-subtraction.  -/
Nat.factorial_mul_ascFactorial' : ∀ (n k : ℕ), 0 < n → (n - 1).factorial * n.ascFactorial k = (n + k - 1).factorial
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.commIsometry_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F],
  (TensorProduct.commIsometry 𝕜 E F).symm = TensorProduct.commIsometry 𝕜 F E
-- Mathlib.CategoryTheory.Conj
CategoryTheory.Iso.conjAut_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f : CategoryTheory.Aut X),
  (α.conjAut f).hom = α.conj f.hom
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.Normal.mem_comm : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.Normal → ∀ {a b : G}, a * b ∈ H → b * a ∈ H
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} [inst_1 : Inhabited (β k)], k ∉ t₂ → (t₁ ∩ t₂).get! k = default
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- Composition of graph homomorphisms.  -/
SimpleGraph.Hom.comp : {V : Type u_1} →
  {W : Type u_2} →
    {X : Type u_3} → {G : SimpleGraph V} → {G' : SimpleGraph W} → {G'' : SimpleGraph X} → G' →g G'' → G →g G' → G →g G''
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.size_left_le_size_union : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp], t₁.size ≤ (t₁ ∪ t₂).size
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.count_map : ∀ {α β β' : Type u_1} [inst : Std.Iterator α Id β] [inst_1 : Std.IteratorLoop α Id Id] [Std.Iterators.Finite α Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {f : β → β'}, (Std.Iter.map f it).length = it.length
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.unop_X₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square Cᵒᵖ),
  sq.unop.X₃ = Opposite.unop sq.X₃
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.two_zsmul_eq_iff : ∀ {ψ θ : Real.Angle}, 2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑Real.pi
-- Mathlib.Tactic.Translate.Reorder
/-- Permute an array of arguments using the given reorder.  -/
Mathlib.Tactic.Translate.ArgReorder.permute! : {α : Type u_1} → [Inhabited α] → Mathlib.Tactic.Translate.ArgReorder → Array α → Array α
-- Mathlib.GroupTheory.Perm.Cycle.Factors
/-- Two permutations `f g : Perm α` have the same cycle factors iff they are the same.  -/
Equiv.Perm.cycleFactorsFinset_injective : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α], Function.Injective Equiv.Perm.cycleFactorsFinset
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_of_mem_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k a : α},
  a ∈ t.erase k → a ∈ t
-- Init.Data.List.MinMaxIdx
List.minIdxOn?_eq_some_minIdxOn : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α} (h : xs ≠ []),
  List.minIdxOn? f xs = some (List.minIdxOn f xs h)
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.spanNorm.congr_simp : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] (I I_1 : Ideal S), I = I_1 → Ideal.spanNorm R I = Ideal.spanNorm R I_1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PullbackCone.IsLimit.lift.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  {t : CategoryTheory.Limits.PullbackCone f g} (ht ht_1 : CategoryTheory.Limits.IsLimit t),
  ht = ht_1 →
    ∀ {W : C} (h h_1 : W ⟶ X) (e_h : h = h_1) (k k_1 : W ⟶ Y) (e_k : k = k_1)
      (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g),
      CategoryTheory.Limits.PullbackCone.IsLimit.lift ht h k w =
        CategoryTheory.Limits.PullbackCone.IsLimit.lift ht_1 h_1 k_1 ⋯
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.addHaarScalarFactor_eq_integral_div_of_continuous_nonneg_pos : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (μ' μ : MeasureTheory.Measure G) [inst_5 : μ.IsAddHaarMeasure]
  [inst_6 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_7 : μ'.IsAddLeftInvariant] {f : C(G, ℝ)},
  HasCompactSupport ⇑f ∧ 0 ≤ f ∧ f 0 ≠ 0 → ↑(μ'.addHaarScalarFactor μ) = (∫ (x : G), f x ∂μ') / ∫ (x : G), f x ∂μ
-- Mathlib.Algebra.Algebra.Unitization
Unitization.starMap_inr : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : NonUnitalSemiring A] [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : SMulCommClass R A A]
  [inst_6 : IsScalarTower R A A] [inst_7 : NonUnitalSemiring B] [inst_8 : StarRing B] [inst_9 : Module R B]
  [inst_10 : SMulCommClass R B B] [inst_11 : IsScalarTower R B B] [inst_12 : StarModule R B] (φ : A →⋆ₙₐ[R] B) (a : A),
  (Unitization.starMap φ) ↑a = ↑(φ a)
-- Mathlib.Algebra.Category.Ring.Adjunctions
/-- `Fun(-, -)` as a functor `Type vᵒᵖ ⥤ CommRingCat ⥤ CommRingCat`.  -/
CommRingCat.coyoneda : CategoryTheory.Functor Type vᵒᵖ (CategoryTheory.Functor CommRingCat CommRingCat)
-- Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
_private.Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv.0.GenContFract.squashGCF.match_3.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Init.Data.Order.Factories
/-- Creates a `Min α` instance from `LE α` and `DecidableLE α` so that `min a b` is either `a` or `b`,
preferring `a` over `b` when in doubt.

Has a `LawfulOrderLeftLeaningMin α` instance.
 -/
Min.leftLeaningOfLE : (α : Type u) → [inst : LE α] → [DecidableLE α] → Min α
-- Mathlib.Algebra.Group.Action.Prod
Prod.isCentralScalar : ∀ {M : Type u_1} {α : Type u_5} {β : Type u_6} [inst : SMul M α] [inst_1 : SMul M β] [inst_2 : SMul Mᵐᵒᵖ α]
  [inst_3 : SMul Mᵐᵒᵖ β] [IsCentralScalar M α] [IsCentralScalar M β], IsCentralScalar M (α × β)
-- Std.Sync.RecursiveMutex
/-- Attempts to lock a `BaseRecursiveMutex`. If the mutex is not available return `false`, otherwise
lock it and return `true`.

This function does not block. Furthermore the same thread may acquire the lock multiple times
through this function.
 -/
Std.BaseRecursiveMutex.tryLock : Std.BaseRecursiveMutex → BaseIO Bool
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.literal : {α : Type} → α → Std.Tactic.BVDecide.BoolExpr α
-- Init.Data.Bool
Bool.cond_self : ∀ {α : Sort u_1} (c : Bool) (t : α), (bif c then t else t) = t
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
/-- If `μ 1 ≤ 1`, then `smoothingFun μ x` is the limit of `smoothingSeminormSeq μ x`
as `n` tends to infinity.  -/
tendsto_smoothingFun_of_map_one_le_one : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R),
  μ 1 ≤ 1 → ∀ (x : R), Filter.Tendsto (smoothingSeminormSeq μ x) Filter.atTop (nhds (smoothingFun μ x))
-- Init.Data.UInt.Bitwise
UInt64.left_le_or : ∀ {a b : UInt64}, a ≤ a ||| b
-- Mathlib.RingTheory.LaurentSeries
/-- The main result showing that the Cauchy filter tends to the `Cauchy.limit`  -/
LaurentSeries.Cauchy.eventually_mem_nhds : ∀ {K : Type u_2} [inst : Field K] {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ) {U : Set (LaurentSeries K)},
  U ∈ nhds (LaurentSeries.Cauchy.limit hℱ) → ∀ᶠ (f : LaurentSeries K) in ℱ, f ∈ U
-- Lean.Elab.ConfigEval.Basic
/-- Calls `EvalConfigItem.setConfig'` from within `runConfigElab`.
 -/
Lean.Elab.ConfigEval.EvalConfigItem.setConfig' : {α : Type} →
  Lean.Elab.ConfigEval.EvalConfigItem α →
    α →
      Lean.Syntax →
        (optParam (α → Lean.Syntax → Lean.Elab.TermElabM α) fun cfg cfgItem =>
            Lean.Elab.ConfigEval.EvalConfigItem.defaultOnErr cfg cfgItem) →
          optParam Bool false → Lean.CoreM α
-- Mathlib.Tactic.FunProp.FunctionData
Mathlib.Meta.FunProp.FunctionData.mk.injEq : ∀ (lctx : Lean.LocalContext) (insts : Lean.LocalInstances) (fn : Lean.Expr) (args : Array Mathlib.Meta.FunProp.Mor.Arg)
  (mainVar : Lean.Expr) (mainArgs : Array ℕ) (lctx_1 : Lean.LocalContext) (insts_1 : Lean.LocalInstances)
  (fn_1 : Lean.Expr) (args_1 : Array Mathlib.Meta.FunProp.Mor.Arg) (mainVar_1 : Lean.Expr) (mainArgs_1 : Array ℕ),
  ({ lctx := lctx, insts := insts, fn := fn, args := args, mainVar := mainVar, mainArgs := mainArgs } =
      { lctx := lctx_1, insts := insts_1, fn := fn_1, args := args_1, mainVar := mainVar_1, mainArgs := mainArgs_1 }) =
    (lctx = lctx_1 ∧ insts = insts_1 ∧ fn = fn_1 ∧ args = args_1 ∧ mainVar = mainVar_1 ∧ mainArgs = mainArgs_1)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey!_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF) {k : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.maxKey! =
    t.maxKey?.elim k fun k' => if compare k' k = Ordering.lt then k else k'
-- Lean.Elab.Do.Basic
Lean.Elab.Do.instInhabitedDoElemContKind.default : Lean.Elab.Do.DoElemContKind
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.mk.sizeOf_spec : ∀ (const : ℤ) (coeffs : Lean.Omega.Coeffs),
  sizeOf { const := const, coeffs := coeffs } = 1 + sizeOf const + sizeOf coeffs
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.instantiateGroundTheorem : Lean.Meta.Grind.EMatchTheorem → Lean.Meta.Grind.EMatch.M Unit
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.ReflQuiv.instInhabited : Inhabited CategoryTheory.ReflQuiv
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
_private.Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass.0.CategoryTheory.ShortComplex.ShortExact.hasSmallLocalizedHom_S'_X₃_K : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] [CategoryTheory.HasExt C]
  {S : CategoryTheory.ShortComplex C},
  S.ShortExact →
    CategoryTheory.Localization.HasSmallLocalizedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ))
      (S.map (CochainComplex.singleFunctor C 0)).X₃
      (CochainComplex.mappingCone (S.map (CochainComplex.singleFunctor C 0)).f)
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.map_neg : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀)
  (x : R), v (-x) = v x
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.le_meet_right : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q : l},
  Lean.Order.PartialOrder.rel P Q → Lean.Order.PartialOrder.rel P (Lean.Order.meet P Q)
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
mdifferentiable_add_section : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {s t : (x : B) → E x},
  MDiff (T% s) → MDiff (T% t) → MDiff fun x => ⟨x, (s + t) x⟩
-- Init.Data.SInt.Bitwise
Int64.zero_shiftRight : ∀ {a : Int64}, 0 >>> a = 0
-- Mathlib.Tactic.Ring.Basic
/-- Turn a NormNum.Result into coefficient data.  -/
Mathlib.Tactic.Ring.RatCoeff.ofResult : {u : Lean.Level} →
  {α : Q(Type u)} →
    {a : Q(«$α»)} →
      Mathlib.Meta.NormNum.Result a → Option (Mathlib.Tactic.Ring.Common.Result Mathlib.Tactic.Ring.RatCoeff a)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toList_roc_ne_zero_iff : ∀ {m n : ℤ} {i : ℕ}, (m<...=n).toList[i]! ≠ 0 ↔ i < (n - m).toNat ∧ m + ↑i ≠ -1
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.zero_vle : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] (x : R), 0 ≤ᵥ x
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.SimpleFunc.integral_eq_integral : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [CompleteSpace E] (f : MeasureTheory.SimpleFunc α E),
  MeasureTheory.Integrable (⇑f) μ → MeasureTheory.SimpleFunc.integral μ f = ∫ (x : α), f x ∂μ
-- Mathlib.Algebra.GroupWithZero.Units.Basic
inv_mul_eq_iff_eq_mul₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b c : G₀}, a ≠ 0 → (a⁻¹ * b = c ↔ b = a * c)
-- Mathlib.Topology.Compactness.Lindelof
Topology.IsClosedEmbedding.LindelofSpace : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [h : LindelofSpace Y] {f : X → Y},
  Topology.IsClosedEmbedding f → LindelofSpace X
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.preprocess : Lean.Expr → Lean.Meta.Grind.GoalM Lean.Meta.Simp.Result
-- Init.Data.List.ToArray
List.isPrefixOfAux_toArray_succ : ∀ {α : Type u_1} [inst : BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : ℕ),
  l₁.toArray.isPrefixOfAux l₂.toArray hle (i + 1) = l₁.tail.toArray.isPrefixOfAux l₂.tail.toArray ⋯ i