mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.Iter.step_filterMapWithPostcondition.match_3.splitter : {α β : Type u_1} →
  [inst : Std.Iterator α Id β] →
    {it : Std.Iter β} →
      (motive : it.Step → Sort u_2) →
        (x : it.Step) →
          ((it' : Std.Iter β) →
              (out : β) →
                (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
            ((it' : Std.Iter β) →
                (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
              ((h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Mathlib.Order.Bounded
Set.bounded_inter_not : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α},
  (∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m) → ∀ (a : α), Set.Bounded r (s ∩ {b | ¬r b a}) ↔ Set.Bounded r s
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.TwoPowShiftTarget.pow : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} → {w : ℕ} → Std.Tactic.BVDecide.BVExpr.bitblast.TwoPowShiftTarget aig w → ℕ
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_p_f : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (α : Type u_3)
  [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α]
  (K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) (ComplexShape.up α)) (n : α),
  ((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).inverse.obj K).p.f n = (K.X n).p
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.toLoop_apply : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] (i : N)
  {p : ↑(GenLoop N X x)} {t : ↑unitInterval} {tn : { j // j ≠ i } → ↑unitInterval},
  ((GenLoop.toLoop i p) t) tn = p ((Cube.insertAt i) (t, tn))
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.getVert_mem_tail_support : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, ¬p.Nil → ∀ {i : ℕ}, i ≠ 0 → p.getVert i ∈ p.support.tail
-- Mathlib.CategoryTheory.Limits.MorphismProperty
CategoryTheory.MorphismProperty.Over.instUniqueHomTopMkId : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    (P : CategoryTheory.MorphismProperty T) →
      {X : T} →
        [inst_1 : P.ContainsIdentities] →
          (Y : P.Over ⊤ X) →
            Unique (Y ⟶ CategoryTheory.MorphismProperty.Over.mk ⊤ (CategoryTheory.CategoryStruct.id X) ⋯)
-- Mathlib.Algebra.Ring.Opposite
MulOpposite.instRing : {R : Type u_1} → [Ring R] → Ring Rᵐᵒᵖ
-- Mathlib.Algebra.Lie.Cochain
LieModule.Cohomology.mem_twoCochain_iff : ∀ {R : Type u_1} [inst : CommRing R] {L : Type u_2} [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {c : L →ₗ[R] L →ₗ[R] M},
  c ∈ LieModule.Cohomology.twoCochain R L M ↔ ∀ (x : L), (c x) x = 0
-- Init.Data.String.Substring
Substring : Type
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.weightMap_weightEquiv_symm : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7}
  [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂] [inst_7 : AddCommGroup N₂] [inst_8 : Module R N₂]
  (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (e : P.Equiv Q) (m : M₂),
  (↑e).weightMap ((RootPairing.Equiv.weightEquiv P Q e).symm m) = m
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.List.findSomeM?_cons.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match none with
    | some b => h_1 b
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
/-- The term in the infinite sum expansion of cot.  -/
cotTerm : ℂ → ℕ → ℂ
-- Mathlib.Order.BooleanAlgebra.Basic
/-- See also `sdiff_inf_right_comm`.  -/
inf_sdiff_assoc : ∀ {α : Type u} [inst : GeneralizedBooleanAlgebra α] (x y z : α), (x ⊓ y) \ z = x ⊓ y \ z
-- Mathlib.Logic.Nonempty
nonempty_pprod : ∀ {α : Sort u_3} {β : Sort u_4}, Nonempty (α ×' β) ↔ Nonempty α ∧ Nonempty β
-- Mathlib.Data.Seq.Parallel
_private.Mathlib.Data.Seq.Parallel.0.Computation.parallel.aux1.match_1.congr_eq_3 : ∀ {α : Type u_1} (motive : Option (Stream'.Seq1 (Option (Computation α))) → Sort u_2)
  (x : Option (Stream'.Seq1 (Option (Computation α)))) (h_1 : Unit → motive none)
  (h_2 : (S' : Stream'.Seq (Option (Computation α))) → motive (some (none, S')))
  (h_3 : (c : Computation α) → (S' : Stream'.Seq (Option (Computation α))) → motive (some (some c, S')))
  (c : Computation α) (S' : Stream'.Seq (Option (Computation α))),
  x = some (some c, S') →
    (match x with
      | none => h_1 ()
      | some (none, S') => h_2 S'
      | some (some c, S') => h_3 c S') ≍
      h_3 c S'
-- Mathlib.Data.Nat.GCD.Basic
Nat.coprime_mul_right_add_right : ∀ (m n k : ℕ), m.Coprime (k * m + n) ↔ m.Coprime n
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.fst_one : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : One α], (NonemptyInterval.toProd 1).1 = 1
-- Mathlib.Topology.Algebra.Monoid
/-- **Alias** of `tendsto_finsetSum`. -/
tendsto_finset_sum : ∀ {ι : Type u_1} {α : Type u_2} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M] [ContinuousAdd M]
  {f : ι → α → M} {x : Filter α} {a : ι → M} (s : Finset ι),
  (∀ i ∈ s, Filter.Tendsto (f i) x (nhds (a i))) → Filter.Tendsto (fun b => ∑ c ∈ s, f c b) x (nhds (∑ c ∈ s, a c))
-- Init.Data.SInt.Lemmas
Int32.neg_ne_zero : ∀ {a : Int32}, -a ≠ 0 ↔ a ≠ 0
-- Mathlib.Data.Rel.Separated
SetRel.IsSeparated.of_subsingleton : ∀ {X : Type u_1} {R : SetRel X X} {s : Set X}, s.Subsingleton → R.IsSeparated s
-- Mathlib.Topology.Separation.Basic
/-- In an R₀ space, the `Specializes` relation is symmetric, `Iff` version.  -/
specializes_comm : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R0Space X] {x y : X}, x ⤳ y ↔ y ⤳ x
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The property that a morphism between additive monoid objects is an additive monoid morphism.  -/
CategoryTheory.IsAddMonHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {M' N' : C} → [CategoryTheory.AddMonObj M'] → [CategoryTheory.AddMonObj N'] → (M' ⟶ N') → Prop
-- Mathlib.Data.Nat.Choose.Lucas
Choose.minFac_sq_ndvd_gcd_choose_of_isPrimePow : ∀ {n : ℕ}, IsPrimePow n → ¬n.minFac ^ 2 ∣ (Finset.Icc 1 (n - 1)).gcd n.choose
-- Mathlib.AlgebraicTopology.DoldKan.Homotopies
/-- The null homotopic map $(hσ q) ∘ d + d ∘ (hσ q)$  -/
AlgebraicTopology.DoldKan.Hσ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X : CategoryTheory.SimplicialObject C} →
        ℕ → (AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ AlgebraicTopology.AlternatingFaceMapComplex.obj X)
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.notMem_nil : ∀ {α : Type u} (a : α), a ∉ Stream'.WSeq.nil
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonLeanFileProgressProcessingInfo : Lean.ToJson Lean.Lsp.LeanFileProgressProcessingInfo
-- Init.Data.UInt.Lemmas
UInt64.toUInt16_ofNatTruncate_of_le : ∀ {n : ℕ},
  UInt64.size ≤ n →
    (UInt64.ofNatClamp n).toUInt16 = UInt16.ofNatLT (UInt16.size - 1) UInt32.toUInt16_ofNatClamp_of_le._proof_1
-- Init.Data.List.Sublist
List.nil_suffix : ∀ {α : Type u_1} {l : List α}, [] <:+ l
-- Init.Data.SInt.Lemmas
Int32.two_mul : ∀ {a : Int32}, 2 * a = a + a
-- Lean.Meta.Tactic.Injection
_private.Lean.Meta.Tactic.Injection.0.Lean.Meta.injectionIntro.go : Bool → ℕ → Lean.MVarId → Array Lean.FVarId → List Lean.Name → Lean.MetaM Lean.Meta.InjectionResult
-- Std.Do.WP.SimpLemmas
Std.Do.WP.modifyGetThe_MonadStateOf : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {σ α : Type u} {Q : Std.Do.PostCond α ps} [inst : Std.Do.WP m ps]
  [inst_1 : MonadStateOf σ m] (f : σ → α × σ),
  (Std.Do.wp (modifyGetThe σ f)).apply Q = (Std.Do.wp (MonadStateOf.modifyGet f)).apply Q
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Real.differentiableWithinAt_arcsin_Ici : ∀ {x : ℝ}, DifferentiableWithinAt ℝ Real.arcsin (Set.Ici x) x ↔ x ≠ -1
-- Mathlib.Analysis.Normed.Group.Uniform
dist_div_eq_dist_mul_right : ∀ {E : Type u_2} [inst : SeminormedCommGroup E] (a b c : E), dist a (b / c) = dist (a * c) b
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.MonOpOpToComonObj_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.Mon Cᵒᵖ), (CategoryTheory.Comon.MonOpOpToComonObj A).X = Opposite.unop A.X
-- Mathlib.Data.Set.Prod
/-- The projection $(X \times_Y Z) \times_Z (X \times_Y Z) \to X \times_Y X$.  -/
Function.PullbackSelf.map_fst : {X : Type u_1} →
  {Y : Sort u_2} →
    {Z : Type u_3} → {f : X → Y} → {g : Z → Y} → Function.PullbackSelf Function.Pullback.snd → Function.PullbackSelf f
-- Mathlib.Order.Filter.AtTopBot.Basic
/-- **Alias** of `Filter.tendsto_atBot_atBot_iff_of_monotone`. -/
Monotone.tendsto_atBot_atBot_iff : ∀ {α : Type u_3} {β : Type u_4} [Nonempty α] [inst : Preorder α] [IsCodirectedOrder α] {f : α → β}
  [inst_2 : Preorder β], Monotone f → (Filter.Tendsto f Filter.atBot Filter.atBot ↔ ∀ (b : β), ∃ a, f a ≤ b)
-- Mathlib.Data.Set.Lattice.Image
Set.surjOn_iUnion_iUnion : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : ι → Set α} {t : ι → Set β} {f : α → β},
  (∀ (i : ι), Set.SurjOn f (s i) (t i)) → Set.SurjOn f (⋃ i, s i) (⋃ i, t i)
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.comapQuotientEquiv.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (c : AddCon M) (f : N →+ M),
  c.comapQuotientEquiv f = (AddCon.congr (AddEquiv.refl N) ⋯).trans (AddCon.quotientKerEquivRange (c.mk'.comp f))
-- Mathlib.Algebra.Torsor.Defs
/-- Simplify division for a torsor for a `Group G` over itself.  -/
sdiv_eq_div : ∀ {G : Type u_1} [inst : Group G] (g₁ g₂ : G), g₁ /ₛ g₂ = g₁ / g₂
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. A measurable function is greater than its mean on a set of positive
measure.  -/
MeasureTheory.measure_laverage_le_pos : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  μ ≠ 0 → ∫⁻ (a : α), f a ∂μ ≠ ⊤ → 0 < μ {x | ⨍⁻ (a : α), f a ∂μ ≤ f x}
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
/-- `monomial` is well-ordered.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.monomialRpow_sorted : ∀ {basis : Tactic.ComputeAsymptotics.Basis} {n : ℕ} {r : ℝ},
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.monomialRpow basis n r).Sorted
-- Mathlib.CategoryTheory.Join.Basic
/-- Characterizing `mapPair` on right morphisms.  -/
CategoryTheory.Join.mapPairRight : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            {E' : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] →
                (Fₗ : CategoryTheory.Functor C E) →
                  (Fᵣ : CategoryTheory.Functor D E') →
                    (CategoryTheory.Join.inclRight C D).comp (CategoryTheory.Join.mapPair Fₗ Fᵣ) ≅
                      Fᵣ.comp (CategoryTheory.Join.inclRight E E')
-- Mathlib.Data.Bool.Basic
Bool.ofNat.eq_1 : ∀ (n : ℕ), Bool.ofNat n = decide (n ≠ 0)
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.comp_id : ∀ {γ : Type u_4} {δ : Type u_5} [inst : TopologicalSpace γ] [inst_1 : TopologicalSpace δ] [inst_2 : Zero δ]
  (f : CompactlySupportedContinuousMap γ δ), f.comp (CocompactMap.id γ) = f
-- Mathlib.GroupTheory.HNNExtension
/-- Two reduced words representing the same element of the `HNNExtension G A B φ` have the same
length corresponding list, with the same pattern of occurrences of `t^1` and `t^(-1)`,
and also the `head` is in the same left coset of `toSubgroup A B (-u)`, where `u : ℤˣ`
is the exponent of the first occurrence of `t` in the word.  -/
HNNExtension.ReducedWord.map_fst_eq_and_of_prod_eq : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {w₁ w₂ : HNNExtension.NormalWord.ReducedWord G A B},
  HNNExtension.NormalWord.ReducedWord.prod φ w₁ = HNNExtension.NormalWord.ReducedWord.prod φ w₂ →
    List.map Prod.fst w₁.toList = List.map Prod.fst w₂.toList ∧
      ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁.head⁻¹ * w₂.head ∈ HNNExtension.toSubgroup A B (-u)
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.toMeasure_injective : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α], Function.Injective PMF.toMeasure
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2.step.match_1.eq_2 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (motive : Turing.TM2.Cfg Γ Λ σ → Sort u_5) (l : Λ)
  (v : σ) (S : (k : K) → List (Γ k))
  (h_1 : (var : σ) → (stk : (k : K) → List (Γ k)) → motive { l := none, var := var, stk := stk })
  (h_2 : (l : Λ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive { l := some l, var := v, stk := S }),
  (match { l := some l, var := v, stk := S } with
    | { l := none, var := var, stk := stk } => h_1 var stk
    | { l := some l, var := v, stk := S } => h_2 l v S) =
    h_2 l v S
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.desc'_inr : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) {X : ι → Type u_5}
  (x₁ : (i₁ : ι₁) → X (e₁.f i₁)) (x₂ : (i₂ : ι₂) → X (e₂.f i₂)) (i : ι₁ ⊕ ι₂) (i₂ : ι₂) (h : Sum.inr i₂ = i),
  ac.desc' x₁ x₂ i = (ComplexShape.Embedding.AreComplementary.desc.aux X (e₂.f i₂) (ac.equiv i) ⋯) (x₂ i₂)
-- Init.Data.String.Pattern.Basic
_private.Init.Data.String.Pattern.Basic.0.String.Slice.Pattern.SearchStep.ofSliceFrom.match_1.splitter : {s : String.Slice} →
  {p : s.Pos} →
    (motive : String.Slice.Pattern.SearchStep (s.sliceFrom p) → Sort u_1) →
      (st : String.Slice.Pattern.SearchStep (s.sliceFrom p)) →
        ((l r : (s.sliceFrom p).Pos) → motive (String.Slice.Pattern.SearchStep.rejected l r)) →
          ((l r : (s.sliceFrom p).Pos) → motive (String.Slice.Pattern.SearchStep.matched l r)) → motive st
-- Mathlib.Order.Preorder.Finsupp
Finsupp.lattice : {ι : Type u_1} → {M : Type u_2} → [inst : Zero M] → [Lattice M] → Lattice (ι →₀ M)
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticRelatedInformation.mk.sizeOf_spec : ∀ (location : Lean.Lsp.Location) (message : String),
  sizeOf { location := location, message := message } = 1 + sizeOf location + sizeOf message
-- Aesop.Tree.Data
Aesop.RappData.state : {Goal MVarCluster : Type} → Aesop.RappData Goal MVarCluster → Aesop.NodeState
-- Mathlib.Combinatorics.Additive.Dissociation
not_mulDissociated_iff_exists_disjoint : ∀ {α : Type u_1} [inst : CommGroup α] {s : Set α},
  ¬MulDissociated s ↔ ∃ t u, ↑t ⊆ s ∧ ↑u ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a
-- Mathlib.Algebra.Group.AddChar
/-- The double dual embedding.  -/
AddChar.doubleDualEmb : {A : Type u_2} → {M : Type u_3} → [inst : AddMonoid A] → [inst_1 : CommMonoid M] → A →+ AddChar (AddChar A M) M
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivWithinAt_one : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) (s : Set 𝕜) [inst_3 : One F], HasDerivWithinAt 1 0 s x
-- Init.Data.UInt.Lemmas
UInt32.toUInt8_ofNatLT : ∀ {n : ℕ} (hn : n < UInt32.size), (UInt32.ofNatLT n hn).toUInt8 = UInt8.ofNat n
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.irreducible_polynomial : ∀ {R : Type r} [inst : CommRing R] {W : WeierstrassCurve.Affine R} [IsDomain R], Irreducible W.polynomial
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Relations.realize_antisymmetric : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {r : L.Relations 2},
  M ⊨ r.antisymmetric ↔ Std.Antisymm fun x y => FirstOrder.Language.Structure.RelMap r ![x, y]
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.cyclesMap_id : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (n : ℕ),
  groupHomology.cyclesMap (MonoidHom.id G) (CategoryTheory.CategoryStruct.id A) n =
    CategoryTheory.CategoryStruct.id (groupHomology.cycles A n)
-- Init.Grind.AC
Lean.Grind.AC.Context : Sort u → Type u
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.instSetLike.eq_1 : ∀ {M : Type u_1} [inst : Mul M], Subsemigroup.instSetLike = { coe := Subsemigroup.carrier, coe_injective := ⋯ }
-- Init.Data.Array.Lemmas
Array.getElem?_filter : ∀ {α : Type u_1} {a : α} {xs : Array α} {p : α → Bool} {i : ℕ},
  i < (Array.filter p xs).size → (Array.filter p xs)[i]? = some a → p a = true
-- Mathlib.MeasureTheory.Measure.OpenPos
/-- **Alias** of `Metric.measure_closedEBall_pos`. -/
EMetric.measure_closedBall_pos : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X)
  [μ.IsOpenPosMeasure] (x : X) {r : ENNReal}, r ≠ 0 → 0 < μ (Metric.closedEBall x r)
-- Mathlib.Algebra.CharP.MixedCharZero
_private.Mathlib.Algebra.CharP.MixedCharZero.0.EqualCharZero.pnatCast_eq_natCast : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))] (n : ℕ+), ↑↑n = ↑↑n
-- Mathlib.Order.WithBot
WithTop.untop_eq_iff : ∀ {α : Type u_1} {a : WithTop α} {b : α} (h : a ≠ ⊤), a.untop h = b ↔ a = ↑b
-- Mathlib.CategoryTheory.RegularCategory.Basic
CategoryTheory.Regular.toHasFiniteLimits : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Regular C],
  CategoryTheory.Limits.HasFiniteLimits C
-- Mathlib.Algebra.DualQuaternion
Quaternion.imK_fst_dualNumberEquiv : ∀ {R : Type u_1} [inst : CommRing R] (q : Quaternion (DualNumber R)),
  (TrivSqZeroExt.fst (Quaternion.dualNumberEquiv q)).imK = TrivSqZeroExt.fst q.imK
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.AccLevelState.mk.injEq : ∀ (levels levels_1 : Lean.LevelMap ℤ), ({ levels := levels } = { levels := levels_1 }) = (levels = levels_1)
-- Mathlib.Algebra.Ring.Parity
odd_neg : ∀ {α : Type u_2} [inst : Ring α] {a : α}, Odd (-a) ↔ Odd a
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- `denoteEntries` is `denote` as a `PArray` for deterministic traversal.  -/
Lean.Meta.Grind.Arith.CommRing.CommRing.denoteEntries : Lean.Meta.Grind.Arith.CommRing.CommRing → Lean.PArray (Lean.Expr × Lean.Meta.Grind.Arith.CommRing.RingExpr)
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex_apply : ∀ {K : Type u_1} [inst : Field K] {v : NumberField.InfinitePlace K} (hv : v.IsComplex) (x : v.Completion),
  (NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex hv) x =
    (NumberField.InfinitePlace.Completion.extensionEmbedding v) x
-- Init.Data.Nat.Lemmas
Nat.sub_add_lt_sub : ∀ {m k n : ℕ}, m + k ≤ n → 0 < k → n - (m + k) < n - m
-- Mathlib.Topology.ContinuousMap.Defs
/-- Coerce a bundled morphism with a `ContinuousMapClass` instance to a `ContinuousMap`.  -/
toContinuousMap : {F : Type u_1} →
  {X : Type u_2} →
    {Y : Type u_3} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] → [inst_2 : FunLike F X Y] → [ContinuousMapClass F X Y] → F → C(X, Y)
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSet.empty : ∀ {α : Type u_1} [inst : MeasurableSpace α], MeasurableSet ∅
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
/-- Given a normed field extension `L / K`, the norm on `L` is a multiplicative `K`-algebra norm.  -/
NormedAlgebra.toMulAlgebraNorm : (K : Type u_1) →
  (L : Type u_2) → [inst : NormedField K] → [inst_1 : NormedField L] → [inst_2 : NormedAlgebra K L] → MulAlgebraNorm K L
-- Mathlib.Topology.LocallyClosed
coborder_preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsOpenMap f → Continuous f → ∀ (s : Set Y), coborder (f ⁻¹' s) = f ⁻¹' coborder s
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.cpow_ofNat : ∀ (x : ℂ) (n : ℕ) [inst : n.AtLeastTwo], x ^ OfNat.ofNat n = x ^ OfNat.ofNat n
-- Mathlib.CategoryTheory.EqToHom
/-- An equality `X = Y` gives us a morphism `X ⟶ Y`.

It is typically better to use this, rather than rewriting by the equality then using `𝟙 _`
which usually leads to dependent type theory hell.
 -/
CategoryTheory.eqToHom : {C : Type u₁} → [inst : CategoryTheory.CategoryStruct.{v₁, u₁} C] → {X Y : C} → X = Y → (X ⟶ Y)
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the largest key in the tree map, returning `fallback` if
the tree map is empty.
 -/
Std.DTreeMap.Raw.maxEntryD : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → (a : α) × β a → (a : α) × β a
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The definition of `vectorSpan`, for rewriting.  -/
vectorSpan_def : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : Set P), vectorSpan k s = Submodule.span k (s -ᵥ s)
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.getStackSize : Lean.PrettyPrinter.FormatterM ℕ
-- Mathlib.Analysis.Calculus.TangentCone.Defs
UniqueDiffOn.uniqueDiffWithinAt : ∀ {R : Type u} {E : Type v} [inst : Semiring R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : TopologicalSpace E] {s : Set E} {x : E}, UniqueDiffOn R s → x ∈ s → UniqueDiffWithinAt R s x
-- Init.Data.Vector.Erase
Vector.getElem_eraseIdx : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} (h : i < n) {j : ℕ} (h' : j < n - 1),
  (xs.eraseIdx i h)[j] = if h'' : j < i then xs[j] else xs[j + 1]
-- Mathlib.Data.Num.Basic
/-- `castZNum` casts a `ZNum` into any type which has `0`, `1`, `+` and `neg`  -/
castZNum : {α : Type u_1} → [Zero α] → [One α] → [Add α] → [Neg α] → ZNum → α
-- Mathlib.LinearAlgebra.SpecialLinearGroup
/-- By base change, an `R`-algebra `S` induces a group homomorphism from
`SpecialLinearGroup R V` to `SpecialLinearGroup S (S ⊗[R] V)`.  -/
SpecialLinearGroup.baseChange : {R : Type u_1} →
  {V : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module R V] →
          {S : Type u_3} →
            [inst_3 : CommRing S] →
              [inst_4 : Algebra R S] →
                [Module.Free R V] →
                  [Module.Finite R V] → SpecialLinearGroup R V →* SpecialLinearGroup S (TensorProduct R S V)
-- Mathlib.Probability.Kernel.Defs
/-- Notation for `Kernel` with respect to a non-standard σ-algebra in the domain and codomain.  -/
ProbabilityTheory.«termKernel[_,_]__» : Lean.ParserDescr
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.HeightOneSpectrum.equivPrimesOver_apply : ∀ {A : Type u_4} [inst : CommRing A] {p : Ideal A} [hpm : p.IsMaximal] (B : Type u_5) [inst_1 : CommRing B]
  [inst_2 : IsDedekindDomain B] [inst_3 : Algebra A B] [inst_4 : IsDomain A] [inst_5 : Module.IsTorsionFree A B]
  (hp : p ≠ 0) (v : { v // v.asIdeal ∣ Ideal.map (algebraMap A B) p }),
  ↑((IsDedekindDomain.HeightOneSpectrum.equivPrimesOver B hp) v) = (↑v).asIdeal
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.finite_range_coeff : ∀ {R : Type u} [inst : Semiring R] (f : Polynomial R), (Set.range f.coeff).Finite
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.comap.eq_1 : ∀ {Ω : Type u_1} {Ω' : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω'] (f : Ω → Ω')
  (μ : MeasureTheory.FiniteMeasure Ω'), MeasureTheory.FiniteMeasure.comap f μ = ⟨MeasureTheory.Measure.comap f ↑μ, ⋯⟩