mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Path
/-- For a path `γ`, `γ.truncate` gives a "continuous family of paths", by which we mean
the uncurried function which maps `(t₀, t₁, s)` to `γ.truncate t₀ t₁ s` is continuous.  -/
Path.truncate_continuous_family : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} (γ : Path a b), Continuous fun x => (γ.truncate x.1 x.2.1) x.2.2
-- Mathlib.Order.CompleteBooleanAlgebra
/-- Pullback a `CompleteDistribLattice` along an injection.  -/
Function.Injective.completeDistribLattice : {α : Type u} →
  {β : Type v} →
    [inst : Max α] →
      [inst_1 : Min α] →
        [inst_2 : LE α] →
          [inst_3 : LT α] →
            [inst_4 : SupSet α] →
              [inst_5 : InfSet α] →
                [inst_6 : Top α] →
                  [inst_7 : Bot α] →
                    [inst_8 : Compl α] →
                      [inst_9 : HImp α] →
                        [inst_10 : HNot α] →
                          [inst_11 : SDiff α] →
                            [inst_12 : CompleteDistribLattice β] →
                              (f : α → β) →
                                Function.Injective f →
                                  (∀ {x y : α}, f x ≤ f y ↔ x ≤ y) →
                                    (∀ {x y : α}, f x < f y ↔ x < y) →
                                      (∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) →
                                        (∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) →
                                          (∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) →
                                            (∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) →
                                              f ⊤ = ⊤ →
                                                f ⊥ = ⊥ →
                                                  (∀ (a : α), f aᶜ = (f a)ᶜ) →
                                                    (∀ (a b : α), f (a ⇨ b) = f a ⇨ f b) →
                                                      (∀ (a : α), f (￢a) = ￢f a) →
                                                        (∀ (a b : α), f (a \ b) = f a \ f b) → CompleteDistribLattice α
-- Mathlib.Order.Hom.Basic
OrderHom.fst_prod_snd : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β], OrderHom.fst.prod OrderHom.snd = OrderHom.id
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.GlobalPreprocessor.mk.inj : ∀ {toPreprocessorBase : Mathlib.Tactic.Linarith.PreprocessorBase}
  {transform : List Lean.Expr → Lean.MetaM (List Lean.Expr)}
  {toPreprocessorBase_1 : Mathlib.Tactic.Linarith.PreprocessorBase}
  {transform_1 : List Lean.Expr → Lean.MetaM (List Lean.Expr)},
  { toPreprocessorBase := toPreprocessorBase, transform := transform } =
      { toPreprocessorBase := toPreprocessorBase_1, transform := transform_1 } →
    toPreprocessorBase = toPreprocessorBase_1 ∧ transform = transform_1
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Methods : Type
-- Mathlib.Topology.Order.Priestley
/-- A Priestley space is an ordered topological space such that any two distinct points can be
separated by a clopen upper set. Compactness is often assumed, but we do not include it here.  -/
PriestleySpace : (α : Type u_2) → [Preorder α] → [TopologicalSpace α] → Prop
-- Mathlib.Topology.Semicontinuity.Defs
HasOpenLowerSections.hasOpenLowerSectionsOn : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β},
  HasOpenLowerSections f → ∀ (s : Set α), HasOpenLowerSectionsOn f s
-- Mathlib.Probability.Distributions.Cauchy
ProbabilityTheory.cauchyMeasure_of_scale_ne_zero : ∀ (x₀ : ℝ) {γ : NNReal},
  γ ≠ 0 → ProbabilityTheory.cauchyMeasure x₀ γ = MeasureTheory.volume.withDensity (ProbabilityTheory.cauchyPDF x₀ γ)
-- Mathlib.RingTheory.HahnSeries.Binomial
HahnSeries.binomial_power : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : AddCommMonoid Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] [inst_4 : BinomialRing R] {x : ↥(HahnSeries.orderTopSubOnePos Γ R)} {r : R},
  x ^ r = HahnSeries.toOrderTopSubOnePos ⋯
-- Mathlib.Data.Nat.Bitwise
Nat.land_assoc : ∀ (n m k : ℕ), n &&& m &&& k = n &&& (m &&& k)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonSemanticTokenModifier.toJson : Lean.Lsp.SemanticTokenModifier → Lean.Json
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.OplaxTrans.Modification.id_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) (a : B),
  (CategoryTheory.Oplax.OplaxTrans.Modification.id η).app a = CategoryTheory.CategoryStruct.id (η.app a)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.neg_comp : ∀ {R : Type u} [inst : Ring R] {p q : Polynomial R}, (-p).comp q = -p.comp q
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.isLocalization_iff_of_ringEquiv : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] (h : S ≃+* P), IsLocalization M S ↔ IsLocalization M P
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.TauPackage.instInhabited : (α : Type u_1) → Inhabited (Besicovitch.TauPackage α α)
-- Mathlib.Data.ENat.Basic
ENat.natCast_ne_coe_top : ∀ (n : ℕ), ↑n ≠ ↑⊤
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.any_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {p : α → β → Bool}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.any p = t₂.any p
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- For `f : α →ᵤ β`, `𝓝 f` admits the family `{g | ∀ x, (f x, g x) ∈ V}` for `V ∈ 𝓤 β` as a
filter basis.  -/
UniformFun.hasBasis_nhds : ∀ (α : Type u_1) (β : Type u_2) [inst : UniformSpace β] (f : UniformFun α β),
  (nhds f).HasBasis (fun V => V ∈ uniformity β) fun V => {g | (f, g) ∈ UniformFun.gen α β V}
-- Aesop.Index.RulePattern
/-- The index.  -/
Aesop.RulePatternIndex.tree : Aesop.RulePatternIndex → Lean.Meta.DiscrTree Aesop.RulePatternIndex.Entry
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.apply_symm_apply : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {x : B × F}, x ∈ e.target → ↑e (↑e.symm x) = x
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.FunIndInfo.mk.injEq : ∀ (funName funIndName : Lean.Name) (levelMask : Array Bool) (params : Array Lean.Meta.FunIndParamKind)
  (funName_1 funIndName_1 : Lean.Name) (levelMask_1 : Array Bool) (params_1 : Array Lean.Meta.FunIndParamKind),
  ({ funName := funName, funIndName := funIndName, levelMask := levelMask, params := params } =
      { funName := funName_1, funIndName := funIndName_1, levelMask := levelMask_1, params := params_1 }) =
    (funName = funName_1 ∧ funIndName = funIndName_1 ∧ levelMask = levelMask_1 ∧ params = params_1)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_inter_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → Std.DHashMap.Raw.Const.get! (m₁ ∩ m₂) k = default
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
CategoryTheory.Limits.hasColimit_fiberwiseColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {H : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} H]
  (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H)
  [inst_2 :
    ∀ {X Y : C} (f : X ⟶ Y),
      CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))]
  [CategoryTheory.Limits.HasColimit G], CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.fiberwiseColimit G)
-- Mathlib.Data.Stream.Init
Stream'.take_drop : ∀ {α : Type u} (m n : ℕ) (a : Stream' α), Stream'.take n (Stream'.drop m a) = List.drop m (Stream'.take (m + n) a)
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.le_addContent_sdiff : ∀ {α : Type u_1} {C : Set (Set α)} {s t : Set α} (m : MeasureTheory.AddContent ENNReal C),
  MeasureTheory.IsSetRing C → s ∈ C → t ∈ C → m s - m t ≤ m (s \ t)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the associator `α_ f g h`.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.associatorM' : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] →
      Mathlib.Tactic.BicategoryLike.Mor₁ →
        Mathlib.Tactic.BicategoryLike.Mor₁ →
          Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.Mor₂Iso
-- Mathlib.Order.SuccPred.Archimedean
/-- **Alias** of `Order.pred_max`. -/
pred_max : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] (a b : α),
  Order.pred (max a b) = max (Order.pred a) (Order.pred b)
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- `StrongRankCondition` implies that if there is an injective linear map `(α →₀ R) →ₗ[R] β →₀ R`,
then the cardinal of `α` is smaller than or equal to the cardinal of `β`.
 -/
card_le_of_injective'' : ∀ {R : Type u} [inst : Semiring R] [StrongRankCondition R] {α β : Type v} (f : (α →₀ R) →ₗ[R] β →₀ R),
  Function.Injective ⇑f → Cardinal.mk α ≤ Cardinal.mk β
-- Mathlib.GroupTheory.Perm.ClosureSwap
Equiv.Perm.IsSwap.finite_compl_fixedBy : ∀ {α : Type u_2} [inst : DecidableEq α] {σ : Equiv.Perm α}, σ.IsSwap → (MulAction.fixedBy α σ)ᶜ.Finite
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.pseudofunctor_mapId : ∀ (C : CategoryTheory.Cat),
  CategoryTheory.WithTerminal.pseudofunctor.mapId C =
    CategoryTheory.Cat.Hom.isoMk (CategoryTheory.WithTerminal.mapId ↑C)
-- Mathlib.Analysis.Calculus.ContDiff.Operations
contDiff_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {n : WithTop ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [inst_3 : NormedCommRing 𝔸']
  [inst_4 : NormedAlgebra 𝕜 𝔸'] {t : Finset ι} {f : ι → E → 𝔸'},
  (∀ i ∈ t, ContDiff 𝕜 n (f i)) → ContDiff 𝕜 n fun y => ∏ i ∈ t, f i y
-- Mathlib.Topology.Maps.Strict.Basic
/-- The identity is a strict map.  -/
Topology.IsStrictMap.id : ∀ {X : Type u_1} [inst : TopologicalSpace X], Topology.IsStrictMap id
-- Mathlib.RingTheory.Congruence.Opposite
RingCon.op_iff : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] {c : RingCon R} {x y : Rᵐᵒᵖ},
  c.op x y ↔ c (MulOpposite.unop y) (MulOpposite.unop x)
-- Std.Internal.Do.Triple.Basic
/-- Pretty-print `Triple` applications back as `⦃ … ⦄` notation.  -/
Std.Internal.Do.unexpandTriple : Lean.PrettyPrinter.Unexpander
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.contains_of_contains_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β},
  (m.insert k v).contains a = true → (k == a) = false → m.contains a = true
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  (hx : AlgebraicIndependent R x) (r : R),
  hx.mvPolynomialOptionEquivPolynomialAdjoin (MvPolynomial.C r) =
    Polynomial.C ((algebraMap R ↥(Algebra.adjoin R (Set.range x))) r)
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.isInvalidContinuationByte_getElem_utf8EncodeChar_one_of_utf8Size_eq_four : ∀ {c : Char} (hc : c.utf8Size = 4),
  ByteArray.utf8DecodeChar?.isInvalidContinuationByte (String.utf8EncodeChar c)[1] = false
-- Mathlib.Geometry.Euclidean.Angle.Incenter
/-- An excenter lying on the internal angle bisector from a vertex is either the incenter or the
excenter opposite that vertex.  -/
Affine.Triangle.eq_incenter_or_eq_excenter_singleton_of_oangle_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {t : Affine.Triangle ℝ P} {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ →
      i₂ ≠ i₃ →
        ∀ {signs : Finset (Fin 3)},
          EuclideanGeometry.oangle (t.points i₂) (t.points i₁) (Affine.Simplex.excenter t signs) =
              EuclideanGeometry.oangle (Affine.Simplex.excenter t signs) (t.points i₁) (t.points i₃) →
            Affine.Simplex.excenter t signs = Affine.Simplex.incenter t ∨
              Affine.Simplex.excenter t signs = Affine.Simplex.excenter t {i₁}
-- Std.Http.Data.URI.Basic
Std.Http.URI.instReprHost : Repr Std.Http.URI.Host
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Comonad.ForgetCreatesColimits'.liftedCoconeIsColimit_desc_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {T : CategoryTheory.Comonad C} (D : CategoryTheory.Functor J T.Coalgebra)
  (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c)
  (s : CategoryTheory.Limits.Cocone D),
  ((CategoryTheory.Comonad.ForgetCreatesColimits'.liftedCoconeIsColimit D c t).desc s).f = t.desc (T.forget.mapCocone s)
-- Mathlib.Order.Heyting.Basic
LE.le.disjoint_compl_left : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, b ≤ a → Disjoint aᶜ b
-- Init.System.IO
/-- Runs an `IO` action in some other `EIO` monad, using `f` to translate `IO` exceptions.
 -/
IO.toEIO : {ε α : Type} → (IO.Error → ε) → IO α → EIO ε α
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
/-- The polar coordinate open partial homeomorphism between the mixed space `ℝ^r₁ × ℂ^r₂` and the polar
space `ℝ^(r₁ + r₂) × ℝ^r₂` defined by sending `x` to `x w` or `‖x w‖` depending on whether `w` is
real or complex for the first component, and to `Arg (x w)`, `w` complex, for the second component.
 -/
NumberField.mixedEmbedding.polarSpaceCoord : (K : Type u_1) →
  [inst : Field K] →
    [NumberField K] →
      OpenPartialHomeomorph (NumberField.mixedEmbedding.mixedSpace K) (NumberField.mixedEmbedding.polarSpace K)
-- Init.MetaTypes
Lean.Meta.Simp.Config.mk.sizeOf_spec : ∀ (maxSteps maxDischargeDepth : ℕ) (contextual memoize singlePass zeta beta eta : Bool)
  (etaStruct : Lean.Meta.EtaStructMode)
  (iota proj decide arith autoUnfold dsimp failIfUnchanged ground unfoldPartialApp zetaDelta index implicitDefEqProofs
    zetaUnused catchRuntime zetaHave letToHave congrConsts bitVecOfNat warnExponents suggestions : Bool)
  (maxSuggestions : Option ℕ) (locals instances : Bool),
  sizeOf
      { maxSteps := maxSteps, maxDischargeDepth := maxDischargeDepth, contextual := contextual, memoize := memoize,
        singlePass := singlePass, zeta := zeta, beta := beta, eta := eta, etaStruct := etaStruct, iota := iota,
        proj := proj, decide := decide, arith := arith, autoUnfold := autoUnfold, dsimp := dsimp,
        failIfUnchanged := failIfUnchanged, ground := ground, unfoldPartialApp := unfoldPartialApp,
        zetaDelta := zetaDelta, index := index, implicitDefEqProofs := implicitDefEqProofs, zetaUnused := zetaUnused,
        catchRuntime := catchRuntime, zetaHave := zetaHave, letToHave := letToHave, congrConsts := congrConsts,
        bitVecOfNat := bitVecOfNat, warnExponents := warnExponents, suggestions := suggestions,
        maxSuggestions := maxSuggestions, locals := locals, instances := instances } =
    1 + sizeOf maxSteps + sizeOf maxDischargeDepth + sizeOf contextual + sizeOf memoize + sizeOf singlePass +
                                                          sizeOf zeta +
                                                        sizeOf beta +
                                                      sizeOf eta +
                                                    sizeOf etaStruct +
                                                  sizeOf iota +
                                                sizeOf proj +
                                              sizeOf decide +
                                            sizeOf arith +
                                          sizeOf autoUnfold +
                                        sizeOf dsimp +
                                      sizeOf failIfUnchanged +
                                    sizeOf ground +
                                  sizeOf unfoldPartialApp +
                                sizeOf zetaDelta +
                              sizeOf index +
                            sizeOf implicitDefEqProofs +
                          sizeOf zetaUnused +
                        sizeOf catchRuntime +
                      sizeOf zetaHave +
                    sizeOf letToHave +
                  sizeOf congrConsts +
                sizeOf bitVecOfNat +
              sizeOf warnExponents +
            sizeOf suggestions +
          sizeOf maxSuggestions +
        sizeOf locals +
      sizeOf instances
-- Init.Data.List.Lemmas
List.mem_ite_nil_left : ∀ {α : Type u_1} {p : Prop} {x : α} [inst : Decidable p] {l : List α}, (x ∈ if p then [] else l) ↔ ¬p ∧ x ∈ l
-- Mathlib.SetTheory.ZFC.PSet
PSet.nonempty_toSet_iff : ∀ {u : PSet.{u_1}}, u.toSet.Nonempty ↔ u.Nonempty
-- Init.Data.UInt.Lemmas
UInt32.toBitVec_neg : ∀ {a : UInt32}, (-a).toBitVec = -a.toBitVec
-- Mathlib.Topology.Order.AtTopBotIxx
/-- A family of half-open intervals bounded by diverging limits is locally finite.  -/
locallyFinite_Ioc_of_tendsto : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {α : Type u_2}
  [inst_3 : LinearOrder α] [LocallyFiniteOrder α] [NoMaxOrder X] [NoMinOrder X] {l u : α → X},
  Filter.Tendsto l Filter.atTop Filter.atTop →
    Filter.Tendsto u Filter.atBot Filter.atBot → LocallyFinite fun n => Set.Ioc (l n) (u n)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.insertNth_apply_below : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} {i j : Fin (n + 1)} (h : j < i) (x : α i) (p : (k : Fin n) → α (i.succAbove k)),
  i.insertNth x p j = ⋯ ▸ p (j.castPred ⋯)
-- Mathlib.Analysis.Calculus.FDeriv.Congr
fderivWithin_congr_set : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s t : Set E},
  s =ᶠ[nhds x] t → fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientAddGroup.instContinuousVAdd : ∀ {G : Type u_2} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [ContinuousAdd G] {N : AddSubgroup G},
  ContinuousVAdd G (G ⧸ N)
-- Mathlib.Data.PFunctor.Univariate.M
/-- destructor for M-types  -/
PFunctor.M.casesOn : {F : PFunctor.{uA, uB}} → {r : F.M → Sort w} → (x : F.M) → ((x : ↑F F.M) → r (PFunctor.M.mk x)) → r x
-- Mathlib.Analysis.Normed.Group.Quotient
/-- An isometric version of `QuotientGroup.quotientBot`.  -/
QuotientGroup.quotientBotIsometryEquiv : {M : Type u_1} → [inst : SeminormedCommGroup M] → M ⧸ ⊥ ≃ᵢ M
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
MvQPF.Cofix.corec₁.eq_1 : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u}
  (g : {X : Type u} → (MvQPF.Cofix F α → X) → (β → X) → β → F (α ::: X)) (x : β),
  MvQPF.Cofix.corec₁ g x = MvQPF.Cofix.corec' (fun x => g Sum.inl Sum.inr x) x
-- Init.Data.Array.Range
Array.range'_concat : ∀ {step s n : ℕ}, Array.range' s (n + 1) step = Array.range' s n step ++ #[s + step * n]
-- Mathlib.Data.Finsupp.MonomialOrder
/-- `syn` is linearly ordered  -/
MonomialOrder.linearOrderSyn : {σ : Type u_1} → (self : MonomialOrder σ) → LinearOrder self.syn
-- Mathlib.Data.Seq.Basic
Stream'.Seq1.instInhabited : {α : Type u} → [Inhabited α] → Inhabited (Stream'.Seq1 α)
-- Mathlib.Order.RelClasses
/-- Set notation form of `LE.le.eq_of_not_lt` -/
LE.le.eq_of_not_ssubset : ∀ {α : Type u_2} [UsesSetNotationForOrder α] [inst : PartialOrder α] {a b : α}, a ⊆ b → ¬a ⊂ b → a = b
-- Mathlib.Data.Real.Basic
/-- `Real.equivCauchy` as a ring equivalence.  -/
Real.ringEquivCauchy : ℝ ≃+* CauSeq.Completion.Cauchy abs
-- Mathlib.LinearAlgebra.Charpoly.Basic
LinearMap.charpoly_natDegree : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [inst_4 : Module.Finite R M] (f : M →ₗ[R] M) [StrongRankCondition R],
  f.charpoly.natDegree = Module.finrank R M
-- Mathlib.Data.Multiset.Functor
Multiset.pure_def : ∀ {α : Type u_1}, pure = singleton
-- Mathlib.LinearAlgebra.BilinearForm.DualLattice
/-- The natural paring of `B.dualSubmodule N` and `N`.
This is bundled as a bilinear map in `BilinForm.dualSubmoduleToDual`.  -/
LinearMap.BilinForm.dualSubmoduleParing : {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : Field S] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Algebra R S] →
              [inst_4 : Module R M] →
                [inst_5 : Module S M] →
                  [inst_6 : IsScalarTower R S M] →
                    (B : LinearMap.BilinForm S M) → {N : Submodule R M} → ↥(B.dualSubmodule N) → ↥N → R
-- Init.Data.Ord.Basic
compareOfLessAndEq_eq_gt_of_lt_iff_not_gt_and_ne : ∀ {α : Type u} [inst : LT α] [LE α] [inst_2 : DecidableLT α] [inst_3 : DecidableEq α] {x y : α},
  (∀ (x y : α), x < y ↔ ¬y < x ∧ x ≠ y) → (compareOfLessAndEq x y = Ordering.gt ↔ y < x)
-- Mathlib.Algebra.Group.Embedding
/-- If left-multiplication by any element is cancellative, left-multiplication by `g` is an
embedding.  -/
mulLeftEmbedding : {G : Type u_1} → [inst : Mul G] → [IsLeftCancelMul G] → G → G ↪ G
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.coe_copy : ∀ {R : Type u} {M : Type v} [inst : SMul R M] (p : SubMulAction R M) (s : Set M) (hs : s = ↑p), ↑(p.copy s hs) = s
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.IsFinitePlace.eq_1 : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (w : AbsoluteValue K ℝ),
  NumberField.IsFinitePlace w = ∃ v, NumberField.place (NumberField.FinitePlace.embedding v) = w
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- Given a Dedekind domain `R` in `K`, its field of fractions, the localization of `R` at
a nonzero prime is a valuation subring of `K`.  -/
IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime : {R : Type u_1} →
  [inst : CommRing R] →
    [IsDedekindDomain R] →
      (K : Type u_2) →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] → [IsFractionRing R K] → IsDedekindDomain.HeightOneSpectrum R → ValuationSubring K
-- Mathlib.RingTheory.QuasiFinite.Basic
PrimeSpectrum.preimageHomeomorphFiber.eq_1 : ∀ (R : Type u_3) (S : Type u_4) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : PrimeSpectrum R),
  PrimeSpectrum.preimageHomeomorphFiber R S p =
    { toEquiv := (PrimeSpectrum.preimageOrderIsoFiber R S p).toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.RingTheory.HopfAlgebra.Basic
HopfAlgebra.counit_comp_antipode : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A],
  CoalgebraStruct.counit ∘ₗ HopfAlgebraStruct.antipode R = CoalgebraStruct.counit
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_inter_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → Std.DTreeMap.Raw.Const.get! (m₁ ∩ m₂) k = default
-- Std.Sat.AIG.LawfulVecOperator
Std.Sat.AIG.LawfulVecOperator.decl_eq : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {β : Std.Sat.AIG α → ℕ → Type}
  {f : {len : ℕ} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len}
  [self : Std.Sat.AIG.LawfulVecOperator α β f] {len : ℕ} (aig : Std.Sat.AIG α) (input : β aig len) (idx : ℕ)
  (h1 : idx < aig.decls.size) (h2 : idx < (f aig input).aig.decls.size), (f aig input).aig.decls[idx] = aig.decls[idx]