mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.equivIco_coe_of_mem : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] {p : 𝕜} [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [hp : Fact (0 < p)] {a : 𝕜} [inst_3 : Archimedean 𝕜] {y : 𝕜},
  y ∈ Set.Ico a (a + p) → ↑((AddCircle.equivIco p a) ↑y) = y
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSet.sUnion : ∀ {α : Type u_1} {m : MeasurableSpace α} {s : Set (Set α)},
  s.Countable → (∀ t ∈ s, MeasurableSet t) → MeasurableSet (⋃₀ s)
-- Mathlib.Topology.Algebra.LinearMapCompletion
ContinuousLinearMap.fromCompletion.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {R₁ : Type u_3} {R₂ : Type u_4} [inst : UniformSpace α] [inst_1 : AddCommGroup α]
  [inst_2 : IsUniformAddGroup α] [inst_3 : Semiring R₁] [inst_4 : Module R₁ α]
  [inst_5 : UniformContinuousConstSMul R₁ α] [inst_6 : Semiring R₂] [inst_7 : UniformSpace β] [inst_8 : AddCommGroup β]
  [inst_9 : IsUniformAddGroup β] [inst_10 : Module R₂ β] [inst_11 : UniformContinuousConstSMul R₂ β] {σ : R₁ →+* R₂}
  [inst_12 : T0Space β] [inst_13 : CompleteSpace β] (f f_1 : α →SL[σ] β),
  f = f_1 → f.fromCompletion = f_1.fromCompletion
-- Mathlib.Analysis.Real.Hyperreal
/-- A hyperreal number is infinite if it is infinite positive or infinite negative.
**Do not use.** Write `ArchimedeanClass.mk x < 0` instead.  -/
Hyperreal.Infinite : ℝ* → Prop
-- Mathlib.Logic.Embedding.Set
Function.Embedding.sigmaSet.congr_simp : ∀ {α : Type u_1} {ι : Type u_2} {s : ι → Set α} (h : Pairwise (Function.onFun Disjoint s)),
  Function.Embedding.sigmaSet h = Function.Embedding.sigmaSet h
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceRErase.eq_6 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (rs : ℕ) (k_1 : α) (v_1 : β k_1)
  (l_1 r_2 : Std.DTreeMap.Internal.Impl α β) (hrb_2 : (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l_1 r_2).Balanced)
  (hlb_1 : Std.DTreeMap.Internal.Impl.leaf.Balanced)
  (hlr_3 :
    Std.DTreeMap.Internal.Impl.BalanceLErasePrecond Std.DTreeMap.Internal.Impl.leaf.size
      (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l_1 r_2).size),
  Std.DTreeMap.Internal.Impl.balanceRErase k v (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l_1 r_2)
      Std.DTreeMap.Internal.Impl.leaf hrb_2 hlb_1 hlr_3 =
    Std.DTreeMap.Internal.Impl.inner (1 + rs) k v (Std.DTreeMap.Internal.Impl.inner rs k_1 v_1 l_1 r_2)
      Std.DTreeMap.Internal.Impl.leaf
-- Std.Time.Format.DateFormat
/-- Midnight string (e.g., "midnight").  -/
Std.Time.DayPeriodSymbols.midnight : Std.Time.DayPeriodSymbols → String
-- Init.Data.List.TakeDrop
_private.Init.Data.List.TakeDrop.0.List.filter.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.Data.List.Basic
List.choose_property : ∀ {α : Type u} (p : α → Prop) [inst : DecidablePred p] (l : List α) (hp : ∃ a ∈ l, p a), p (List.choose p l hp)
-- Mathlib.Algebra.Group.Int.Units
Int.mul_eq_one_iff_eq_one_or_neg_one : ∀ {u v : ℤ}, u * v = 1 ↔ u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1
-- Lean.Elab.BuiltinNotation
Lean.Elab.Term.elabCoe : Lean.Elab.Term.TermElab
-- Std.Internal.Do.WP.Lemmas
_private.Std.Internal.Do.WP.Lemmas.0.Std.Internal.Do.Except.wpInst.match_1.eq_2 : ∀ {ε : Type u_1} {α : Type u_2} (motive : Except ε α → Sort u_3) (el : ε) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (el : ε) → motive (Except.error el)),
  (match Except.error el with
    | Except.ok a => h_1 a
    | Except.error el => h_2 el) =
    h_2 el
-- Init.Data.Array.MinMax
List.max_toArray : ∀ {α : Type u_1} [inst : Max α] {l : List α} {h : l.toArray ≠ #[]}, l.toArray.max h = l.max ⋯
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Alt.ref : {σ : Type} → Lean.Elab.Term.Do.Alt σ → Lean.Syntax
-- Mathlib.CategoryTheory.Sums.Basic
/-- The sum `F.sum' G` precomposed with the left inclusion functor is isomorphic to `F`  -/
CategoryTheory.Functor.inlCompSum' : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            (F : CategoryTheory.Functor A C) →
              (G : CategoryTheory.Functor B C) → (CategoryTheory.Sum.inl_ A B).comp (F.sum' G) ≅ F
-- Mathlib.Algebra.ContinuedFractions.Computation.Approximations
/-- Shows that the fractional parts of the stream are in `[0,1)`.  -/
GenContFract.IntFractPair.nth_stream_fr_nonneg_lt_one : ∀ {K : Type u_1} {v : K} {n : ℕ} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K]
  [inst_3 : FloorRing K] {ifp_n : GenContFract.IntFractPair K},
  GenContFract.IntFractPair.stream v n = some ifp_n → 0 ≤ ifp_n.fr ∧ ifp_n.fr < 1
-- Init.System.IO
/-- Terminates the current process with the provided exit code. `0` indicates success, all other values
indicate failure.
 -/
IO.Process.exit : {α : Type} → UInt8 → IO α
-- Mathlib.Topology.Order.Monotone
IsClosed.sInf_mem : ∀ {α : Type u_1} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] {s : Set α},
  s.Nonempty → IsClosed s → sInf s ∈ s
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.size_le_size_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α}, t.size ≤ (t.insert k).size
-- Lean.LibrarySuggestions.Basic
/-- A filter on suggestions; only suggestions returning `true` should be returned.
(It can be better to filter on the premise selection side, to ensure that enough suggestions are returned.)
 -/
Lean.LibrarySuggestions.Config.filter : Lean.LibrarySuggestions.Config → Lean.Name → Lean.MetaM Bool
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.map_val_atTop_of_Ici_subset : ∀ {α : Type u_3} [inst : Preorder α] [IsDirectedOrder α] {a : α} {s : Set α},
  Set.Ici a ⊆ s → Filter.map Subtype.val Filter.atTop = Filter.atTop
-- Init.ShareCommon
ShareCommon.StateFactoryImpl.mapFind? : (self : ShareCommon.StateFactoryImpl) → self.Map → ShareCommon.Object → Option ShareCommon.Object
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.elabNestedAction : Lean.Elab.Term.TermElab
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- The `n`-cliques in a graph as a finset.  -/
SimpleGraph.cliqueFinset : {α : Type u_1} → (G : SimpleGraph α) → [Fintype α] → [DecidableEq α] → [DecidableRel G.Adj] → ℕ → Finset (Finset α)
-- Mathlib.Analysis.Complex.JensenFormula
_private.Mathlib.Analysis.Complex.JensenFormula.0.continuous_herglotzLogIntegrand_circle : ∀ {w ρ : ℂ} {R r : ℝ}, ‖ρ‖ = R → r < R → ‖w‖ < r → Continuous fun θ => herglotzLogIntegrand✝ w ρ (circleMap 0 r θ)
-- Lean.Data.SMap
Lean.SMap.find! : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → [Inhabited β] → Lean.SMap α β → α → β
-- Mathlib.Order.Shrink
equivShrink_top : ∀ {α : Type u_1} [inst : Small.{u, u_1} α] [inst_1 : Top α], (equivShrink α) ⊤ = ⊤
-- Mathlib.Topology.Algebra.StarSubalgebra
StarSubalgebra.map_topologicalClosure_le : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : StarRing A]
  [inst_6 : StarModule R A] [inst_7 : IsSemitopologicalSemiring A] [inst_8 : ContinuousStar A]
  [inst_9 : TopologicalSpace B] [inst_10 : Semiring B] [inst_11 : Algebra R B] [inst_12 : StarRing B]
  [inst_13 : StarModule R B] [inst_14 : IsSemitopologicalSemiring B] [inst_15 : ContinuousStar B]
  (s : StarSubalgebra R A) (φ : A →⋆ₐ[R] B),
  Continuous ⇑φ → StarSubalgebra.map φ s.topologicalClosure ≤ (StarSubalgebra.map φ s).topologicalClosure
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.instHasPushoutHomDiscretePUnitOfHasPushoutsAlong : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T) {X Y : T}
  (f : X ⟶ Y) [P.HasPushoutsAlong f] (A : P.Under Q X), CategoryTheory.Limits.HasPushout A.hom f
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.IsAtom.eq_of_inter_nonempty : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {A B S : Finset G},
  K ≤ 1 → S.Nonempty → Finset.IsAtom✝ K S A → Finset.IsAtom✝ K S B → (A ∩ B).Nonempty → A = B
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_erase_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.erase k).getKey? k = none
-- Init.Internal.Order.Lemmas
Lean.Order.Array.monotone_findRevM? : ∀ {γ : Type w} [inst : Lean.Order.PartialOrder γ] {m : Type → Type v} [inst_1 : Monad m]
  [inst_2 : (α : Type) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m] {α : Type} (f : γ → α → m Bool)
  (xs : Array α), Lean.Order.monotone f → Lean.Order.monotone fun x => Array.findRevM? (f x) xs
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.beth_add_one : ∀ (o : Ordinal.{u_1}), Cardinal.beth (o + 1) = 2 ^ Cardinal.beth o
-- Mathlib.CategoryTheory.Monad.Monadicity
/-- Provided we have the appropriate coequalizers, we have an adjunction to the comparison functor.
 -/
CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {G : CategoryTheory.Functor D C} →
          {F : CategoryTheory.Functor C D} →
            (adj : F ⊣ G) →
              [inst_2 :
                  ∀ (A : adj.toMonad.Algebra),
                    CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] →
                CategoryTheory.Monad.MonadicityInternal.leftAdjointComparison adj ⊣ CategoryTheory.Monad.comparison adj
-- Mathlib.Algebra.Order.ToIntervalMod
AddCommGroup.tfae_modEq : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α),
  [a ≡ b [PMOD p], ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p), toIcoMod hp a b ≠ toIocMod hp a b,
      toIcoMod hp a b + p = toIocMod hp a b].TFAE
-- Mathlib.RingTheory.Extension.Presentation.Submersive
/-- The Jacobian of a `P : PreSubmersivePresentation` is the determinant
of `P.differential` viewed as element of `S`.  -/
Algebra.PreSubmersivePresentation.jacobian : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Algebra.PreSubmersivePresentation R S ι σ → [Finite σ] → S
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_mul_eq_right_of_isLowerTriangular : ∀ {m : Type um} {n : Type un} [inst : Fintype n] {R : Type u_1} [inst_1 : CommRing R] [IsDomain R] [inst_3 : Fintype m]
  [inst_4 : LinearOrder m] (A : Matrix m m R) (B : Matrix m n R),
  A.IsLowerTriangular → (∀ (i : m), A.diag i ≠ 0) → (A * B).rank = B.rank
-- Init.Data.Rat.Basic
Rat.sub.aux : ∀ (a b : ℚ) {g ad bd : ℕ},
  g = a.den.gcd b.den →
    ad = a.den / g →
      bd = b.den / g →
        have den := ad * b.den;
        have num := a.num * ↑bd - b.num * ↑ad;
        num.natAbs.gcd g = num.natAbs.gcd den
-- Mathlib.CategoryTheory.Monoidal.Types.Basic
CategoryTheory.instBraidedCategoryType : CategoryTheory.BraidedCategory (Type u)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
SimplexCategoryGenRel.instIsSplitMonoδ : ∀ {n : ℕ} {i : Fin (n + 2)}, CategoryTheory.IsSplitMono (SimplexCategoryGenRel.δ i)
-- Init.Data.ByteArray.Lemmas
ByteArray.extract_append_eq_left : ∀ {a b : ByteArray} {i : ℕ}, i = a.size → (a ++ b).extract 0 i = a
-- Mathlib.Analysis.SpecificLimits.Normed
/-- For any natural `k` and a real `r > 1` we have `n ^ k = o(r ^ n)` as `n → ∞`.  -/
isLittleO_pow_const_const_pow_of_one_lt : ∀ {R : Type u_2} [inst : NormedRing R] (k : ℕ) {r : ℝ}, 1 < r → (fun n => ↑n ^ k) =o[Filter.atTop] fun n => r ^ n
-- Mathlib.Order.BoundedOrder.Monotone
antitone_lt : ∀ {α : Type u} [inst : Preorder α] {x : α}, Antitone fun x_1 => x_1 < x
-- Mathlib.Analysis.Complex.Schwarz
/-- Two cases of the **Schwarz Lemma** (derivative and distance), merged together.

If `f : ℂ → E` is a complex analytic function on an open ball `ball c R₁`
hat sends it to a closed ball `closedBall (f c) R₂`, then the norm of `dslope f c z`,
which is defined as `(z - c)⁻¹ • (f z - f c)` for `z ≠ c` and as `deriv f c` for `z = c`,
is not greater than the ratio `R₂ / R₁`.
 -/
Complex.norm_dslope_le_div_of_mapsTo_ball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {R₁ R₂ : ℝ} {f : ℂ → E} {c z : ℂ},
  DifferentiableOn ℂ f (Metric.ball c R₁) →
    Set.MapsTo f (Metric.ball c R₁) (Metric.closedBall (f c) R₂) → z ∈ Metric.ball c R₁ → ‖dslope f c z‖ ≤ R₂ / R₁
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R)
  (x : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)), ↑(r • x) = r • ↑x
-- Init.Data.List.Basic
List.eraseRepsBy.loop : {α : Type u_1} → (α → α → Bool) → α → List α → List α → List α
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
IsKleinFour.eq_finset_univ : ∀ {G : Type u_1} [inst : Group G] [IsKleinFour G] [inst_2 : Fintype G] [inst_3 : DecidableEq G] {x y : G},
  x ≠ 1 → y ≠ 1 → x ≠ y → {x * y, x, y, 1} = Finset.univ
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.map_pow : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀)
  (x : R) (n : ℕ), v (x ^ n) = n • v x
-- Mathlib.Algebra.Module.Presentation.Tautological
Module.Presentation.tautological.R.smul.inj : ∀ {A : Type u} {M : Type v} {a : A} {m : M} {a_1 : A} {m_1 : M},
  Module.Presentation.tautological.R.smul a m = Module.Presentation.tautological.R.smul a_1 m_1 → a = a_1 ∧ m = m_1
-- Mathlib.Topology.NhdsWithin
nhdsWithin_inter : ∀ {α : Type u_1} [inst : TopologicalSpace α] (a : α) (s t : Set α),
  nhdsWithin a (s ∩ t) = nhdsWithin a s ⊓ nhdsWithin a t
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `Submodule.projection_eq_self_sub_projection`. -/
Submodule.IsCompl.projection_eq_self_sub_projection : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q) (x : E), (q.projection p ⋯) x = x - (p.projection q hpq) x
-- Lean.Elab.Command
Lean.Elab.Command.State.auxDeclNGen : Lean.Elab.Command.State → Lean.DeclNameGenerator
-- Init.Grind.ToInt
_private.Init.Grind.ToInt.0.Lean.Grind.instBEqIntInterval.beq_spec_3 : ∀ (a b : ℤ), (Lean.Grind.IntInterval.io a == Lean.Grind.IntInterval.io b) = (a == b)
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- For an inclusion `i : V ⟶ U` between open sets of the prime spectrum of `R`, the comap of the
identity from OO_X(U) to OO_X(V) equals as the restriction map of the structure sheaf.

This is a generalization of the fact that, for fixed `U`, the comap of the identity from OO_X(U)
to OO_X(U) is the identity.
 -/
AlgebraicGeometry.StructureSheaf.comap_id_eq_map : ∀ {R : Type u} [inst : CommRing R] (U V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (iVU : V ⟶ U),
  AlgebraicGeometry.StructureSheaf.comap (RingHom.id R) U V ⋯ =
    CommRingCat.Hom.hom ((AlgebraicGeometry.Spec.structureSheaf R).obj.map iVU.op)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.red_negRev_iff : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)},
  FreeAddGroup.Red (FreeAddGroup.negRev L₁) (FreeAddGroup.negRev L₂) ↔ FreeAddGroup.Red L₁ L₂
-- Mathlib.LinearAlgebra.CliffordAlgebra.Inversion
/-- For a vector with invertible quadratic form, $v^{-1} = \frac{v}{Q(v)}$  -/
CliffordAlgebra.invOf_ι : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (m : M) [inst_3 : Invertible (Q m)] [inst_4 : Invertible ((CliffordAlgebra.ι Q) m)],
  ⅟((CliffordAlgebra.ι Q) m) = (CliffordAlgebra.ι Q) (⅟(Q m) • m)
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.Comonad.Coalgebra.isoMk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A B : G.Coalgebra}
  (h h_1 : A.A ≅ B.A) (e_h : h = h_1)
  (w : CategoryTheory.CategoryStruct.comp A.a (G.map h.hom) = CategoryTheory.CategoryStruct.comp h.hom B.a),
  CategoryTheory.Comonad.Coalgebra.isoMk h w = CategoryTheory.Comonad.Coalgebra.isoMk h_1 ⋯
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.of : (carrier : Type u) → [str : MeasurableSpace carrier] → SFinKer
-- Init.Data.Fin.Lemmas
Fin.zero_mul : ∀ {n : ℕ} [inst : NeZero n] (k : Fin n), 0 * k = 0
-- Mathlib.Order.Monotone.Basic
monotone_add_nat_iff_monotoneOn_nat_Ici : ∀ {α : Type u} [inst : Preorder α] {f : ℕ → α} {k : ℕ}, (Monotone fun n => f (n + k)) ↔ MonotoneOn f {x | k ≤ x}
-- Mathlib.Data.Multiset.UnionInter
Multiset.disjoint_singleton : ∀ {α : Type u_1} {l : Multiset α} {a : α}, Disjoint l {a} ↔ a ∉ l
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.tr.eq_10 : ∀ (f : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.comp f k)) =
    Turing.TM2.Stmt.goto fun x => Turing.PartrecToTM2.trNormal f k
-- Std.Http.Data.Headers
Std.Http.Headers.instForInProdNameValueOfMonad : {m : Type u_1 → Type u_2} → [Monad m] → ForIn m Std.Http.Headers (Std.Http.Header.Name × Std.Http.Header.Value)
-- Init.Data.SInt.Bitwise
instCommutativeISizeHAnd : Std.Commutative fun x1 x2 => x1 &&& x2
-- Mathlib.Data.Nat.Factorial.Basic
Nat.ascFactorialBinary.match_1.congr_eq_2 : ∀ (motive : ℕ → Sort u_1) (k : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1)
  (h_3 : (k n : ℕ) → k = n + 2 → motive n.succ.succ),
  k = 1 →
    (match k with
      | 0 => h_1 ()
      | 1 => h_2 ()
      | k@h:n.succ.succ => h_3 k n h) ≍
      h_2 ()
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.foldrM_eq_foldrM_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w'} {β : Type v}
  {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ},
  Std.DTreeMap.Raw.foldrM f init t = Array.foldrM (fun a b => f a.1 a.2 b) init (Std.DTreeMap.Raw.Const.toArray t)
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.inv_mem_resolventSet : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : Rˣ} {a : Aˣ},
  ↑r ∈ resolventSet R ↑a → ↑r⁻¹ ∈ resolventSet R ↑a⁻¹
-- Init.Data.List.Nat.Modify
List.modify_eq_take_cons_drop : ∀ {α : Type u_1} {f : α → α} {i : ℕ} {l : List α} (h : i < l.length),
  l.modify i f = List.take i l ++ f l[i] :: List.drop (i + 1) l
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.continuous_coe : Continuous Complex.UnitClosedDisc.coe
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
tprod_eq_one_of_not_multipliable : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β} {f : β → α},
  ¬Multipliable f L → ∏'[L] (b : β), f b = 1
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.iSup_genEigenspace_eq : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M)
  (μ : R), ⨆ k, (f.genEigenspace μ) ↑k = f.maxGenEigenspace μ
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.ofMonoidHom.sizeOf_spec : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Monoid G] [inst_1 : Ring R] [inst_2 : AddCommGroup V]
  [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V] [inst_6 : SizeOf R]
  [inst_7 : SizeOf G] [inst_8 : SizeOf V] (toMonoidHom : G →* V →L[R] V),
  sizeOf { toMonoidHom := toMonoidHom } = 1 + sizeOf toMonoidHom
-- Mathlib.Tactic.Abel
/-- Auxiliary function for `evalSMul'`.
 -/
Mathlib.Tactic.Abel.evalSMul : Lean.Expr × ℤ → Mathlib.Tactic.Abel.NormalExpr → Mathlib.Tactic.Abel.M (Mathlib.Tactic.Abel.NormalExpr × Lean.Expr)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.inv_μ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X Y : C),
  CategoryTheory.inv (CategoryTheory.Functor.LaxMonoidal.μ F X Y) = CategoryTheory.Functor.OplaxMonoidal.δ F X Y
-- Mathlib.AlgebraicGeometry.Morphisms.Constructors
/-- `topologically P` holds for a morphism if the underlying topological map satisfies `P`.  -/
AlgebraicGeometry.topologically : ({α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop) →
  CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolutionExtensionUnit_comp_ι_map_whiskerLeft_app : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} (V : Type u₂) {inst_1 : CategoryTheory.Category.{v₂, u₂} V}
  {inst_2 : CategoryTheory.MonoidalCategory C} {inst_3 : CategoryTheory.MonoidalCategory V} {D : Type u₃}
  {inst_4 : CategoryTheory.Category.{v₃, u₃} D} {inst_5 : CategoryTheory.MonoidalCategoryStruct D}
  [self : CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct C V D] (d₁ : D) {d₂ d₂' : D}
  (f₂ : d₂ ⟶ d₂') (x y : C),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolutionExtensionUnit C V d₁
            d₂).app
        (x, y))
      (((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).map
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft d₁ f₂)).app
        (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
        (((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d₁).obj x)
        (((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).map f₂).app y))
      ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolutionExtensionUnit C V d₁
            d₂').app
        (x, y))
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerLeft_iff : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} (η θ : f ⟶ g),
  CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id a) η =
      CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id a) θ ↔
    η = θ
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.Pattern.mk.congr_simp : ∀ {A : Type u_1} {G : Type u_2} [inst : Inhabited A] (config config_1 : G → A) (e_config : config = config_1)
  (support support_1 : Finset G) (e_support : support = support_1) (condition : ∀ g ∉ support, config g = default),
  { config := config, support := support, condition := condition } =
    { config := config_1, support := support_1, condition := ⋯ }
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.erase.match_1.splitter : {α : Type u_1} →
  (as : Array α) →
    (motive : Option (Fin as.size) → Sort u_2) →
      (x : Option (Fin as.size)) → (Unit → motive none) → ((i : Fin as.size) → motive (some i)) → motive x
-- Aesop.Stats.Basic
Aesop.Stats.ruleSetConstruction : Aesop.Stats → Aesop.Nanos
-- Mathlib.GroupTheory.Perm.Centralizer
/-- For each cycle, the chosen element belongs to the cycle  -/
Equiv.Perm.Basis.mem_support_self' : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} (self : g.Basis)
  (c : ↥g.cycleFactorsFinset), self.toFun c ∈ (↑c).support
-- Mathlib.Order.BourbakiWitt
ChainCompletePartialOrder.IsExtremePt.mem_bot_iff_isExtremePt : ∀ {α : Type u_1} [inst : ChainCompletePartialOrder α] {x : α} {f : α → α} {y : α},
  (∀ (x : α), x ≤ f x) → (y ∈ ChainCompletePartialOrder.bot x f ↔ ChainCompletePartialOrder.IsExtremePt x f y)