mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.DerivationBundle
PointedContMDiffMap.instIsScalarTowerSomeENatTop : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] (x : M),
  IsScalarTower 𝕜 (PointedContMDiffMap 𝕜 I M (↑⊤) x) 𝕜
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.isOpen_Ico_zero : ∀ {b : ENNReal}, IsOpen (Set.Ico 0 b)
-- Init.Data.Int.Gcd
Int.gcd_self_sub_left : ∀ (m n : ℤ), (m - n).gcd m = n.gcd m
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (not_mem : k ∉ t₂) {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂).getKey k h' = t₁.getKey k ⋯
-- Lean.Meta.Tactic.Grind.PP
/-- Helper function for pretty printing the state for debugging purposes.  -/
_private.Lean.Meta.Tactic.Grind.PP.0.Lean.Meta.Grind.Goal.ppENodeDeclValue : Lean.Meta.Grind.Goal → Lean.Expr → Lean.MetaM Lean.MessageData
-- Init.Data.Range.Polymorphic.Map
Std.PRange.UpwardEnumerable.Map.PreservesLeast?.mk : ∀ {α : Type u_1} {β : Type u_2} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.UpwardEnumerable β]
  [inst_2 : Std.PRange.Least? α] [inst_3 : Std.PRange.Least? β] {f : Std.PRange.UpwardEnumerable.Map α β},
  Option.map f.toFun Std.PRange.least? = Std.PRange.least? → f.PreservesLeast?
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_surjective : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S],
  Function.Surjective fun x =>
    match x with
    | (r, m) => IsLocalization.mk' S r m
-- Mathlib.NumberTheory.Height.Basic
/-- Eta-expanded form of `Height.mulHeight_zero` -/
Height.fun_mulHeight_zero : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2},
  (Height.mulHeight fun x => 0) = 1
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.toBoundedContinuousFunctionLM_eq_of_scalars : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (𝕜' : Type u_5)
  [inst_7 : NontriviallyNormedField 𝕜'] [inst_8 : NormedSpace 𝕜' F] [inst_9 : SMulCommClass ℝ 𝕜' F],
  ⇑(ContDiffMapSupportedIn.toBoundedContinuousFunctionLM 𝕜) = ⇑(ContDiffMapSupportedIn.toBoundedContinuousFunctionLM 𝕜')
-- Init.Data.BitVec.Lemmas
BitVec.zero_eq_allOnes_iff : ∀ {w : ℕ}, 0#w = BitVec.allOnes w ↔ w = 0
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeSortTR.run.match_3.eq_1 : ∀ {α : Type u_1} (motive : (x : ℕ) → { l // l.length = x } → Sort u_2) (property : [].length = 0)
  (h_1 : (property : [].length = 0) → motive 0 ⟨[], property⟩)
  (h_2 : (a : α) → (property : [a].length = 1) → motive 1 ⟨[a], property⟩)
  (h_3 : (n : ℕ) → (xs : { l // l.length = n + 2 }) → motive n.succ.succ xs),
  (match 0, ⟨[], property⟩ with
    | 0, ⟨[], property⟩ => h_1 property
    | 1, ⟨[a], property⟩ => h_2 a property
    | n.succ.succ, xs => h_3 n xs) =
    h_1 property
-- Mathlib.Data.Prod.Basic
Prod.map_injective : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Nonempty α] [Nonempty β] {f : α → γ} {g : β → δ},
  Function.Injective (Prod.map f g) ↔ Function.Injective f ∧ Function.Injective g
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.insertMany_list_eq_foldl : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)}, m.insertMany l = List.foldl (fun acc p => acc.insert p.1 p.2) m l
-- Mathlib.Data.Ordmap.Ordnode
/-- O(m * log(|m ∪ n| + 1)), m ≤ n. Intersection of two sets, preferring members of
`t₁` over those of `t₂` when equivalent elements are encountered.

```
inter {1, 2} {2, 3} = {2}
inter {1, 3} {2} = ∅
```  -/
Ordnode.inter : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → Ordnode α → Ordnode α → Ordnode α
-- Mathlib.CategoryTheory.Limits.Unit
/-- Any cocone over a functor into `PUnit` is a colimit cocone.
 -/
CategoryTheory.Limits.punitCoconeIsColimit : {J : Type v} →
  [inst : CategoryTheory.Category.{v', v} J] →
    {F : CategoryTheory.Functor J (CategoryTheory.Discrete PUnit.{u_1 + 1})} →
      {c : CategoryTheory.Limits.Cocone F} → CategoryTheory.Limits.IsColimit c
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- The projection map is surjective.  -/
AddGroupExtension.rightHom_surjective : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  (self : AddGroupExtension N E G), Function.Surjective ⇑self.rightHom
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The `v`-adic valuation on `R` is bounded above by 1.  -/
IsDedekindDomain.HeightOneSpectrum.intValuation_le_one : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (x : R),
  v.intValuation x ≤ 1
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.coe_pow : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (e : X ≃ᵈ X) (n : ℕ), ⇑(e ^ n) = (⇑e)^[n]
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Pos.revSkipWhile_eq_revSkipWhile_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String} {pos : s.Pos},
  pos.revSkipWhile pat = String.Pos.ofToSlice (pos.toSlice.revSkipWhile pat)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.YClass.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Affine R) (y : Polynomial R),
  WeierstrassCurve.Affine.CoordinateRing.YClass W' y =
    (WeierstrassCurve.Affine.CoordinateRing.mk W') (Polynomial.X - Polynomial.C y)
-- Mathlib.AlgebraicGeometry.Noetherian
AlgebraicGeometry.IsNoetherian.toCompactSpace : ∀ {X : AlgebraicGeometry.Scheme} [self : AlgebraicGeometry.IsNoetherian X], CompactSpace ↥X
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k k' : α},
  (k == k') = true →
    ∀ {v fallback : β},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l → (k, v) ∈ l → (m.insertMany l).getD k' fallback = v
-- Mathlib.Order.WellFounded
/-- The supremum of a bounded, well-founded order  -/
WellFounded.sup : {α : Type u_1} → {r : α → α → Prop} → WellFounded r → (s : Set α) → Set.Bounded r s → α
-- Mathlib.Analysis.Complex.MeanValue
/-- The **Mean Value Property** of complex differentiable functions: If `f : ℂ → E` is continuous on a
closed disc of radius `R` and center `c`, and is complex differentiable at all but countably many
points of its interior, then the circle average `circleAverage f c R` equals `f c`.
 -/
circleAverage_of_differentiable_on_off_countable : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {R : ℝ} {c : ℂ}
  {s : Set ℂ},
  s.Countable →
    ContinuousOn f (Metric.closedBall c |R|) →
      (∀ z ∈ Metric.ball c |R| \ s, DifferentiableAt ℂ f z) → Real.circleAverage f c R = f c
-- Mathlib.Order.Defs.Unbundled
ne_of_irrefl : ∀ {α : Sort u_1} {r : α → α → Prop} [Std.Irrefl r] {x y : α}, r x y → x ≠ y
-- Lean.Meta.KExprMap
Lean.Meta.KExprMap.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (map : Lean.PHashMap Lean.HeadIndex (Lean.AssocList Lean.Expr α)),
  sizeOf { map := map } = 1 + sizeOf map
-- Mathlib.Algebra.Lie.Basic
LieEquiv.hasCoeToLinearEquiv : {R : Type u} →
  {L₁ : Type v} →
    {L₂ : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L₁] →
          [inst_2 : LieRing L₂] →
            [inst_3 : LieAlgebra R L₁] → [inst_4 : LieAlgebra R L₂] → Coe (L₁ ≃ₗ⁅R⁆ L₂) (L₁ ≃ₗ[R] L₂)
-- Mathlib.Logic.Function.Basic
Function.uncurry_injective : ∀ {α : Type u_1} {β : Type u_2} {γ : Sort u_3}, Function.Injective Function.uncurry
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
/-- If a group with zero `G₀` acts on `α` by measurable maps, then each nonzero element `c : G₀`
defines a measurable automorphism of `α`  -/
MeasurableEquiv.smul₀ : {G₀ : Type u_2} →
  {α : Type u_3} →
    [inst : MeasurableSpace α] →
      [inst_1 : GroupWithZero G₀] → [inst_2 : MulAction G₀ α] → [MeasurableConstSMul G₀ α] → (c : G₀) → c ≠ 0 → α ≃ᵐ α
-- Mathlib.Topology.Order.IntermediateValue
Continuous.image_Ioc_of_strictMono : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a b : α} {f : α → δ}, Continuous f → StrictMono f → f '' Set.Ioc a b = Set.Ioc (f a) (f b)
-- Std.Async.UDP
/-- Sets the multicast interface for sending packets.
 -/
Std.Async.UDP.Socket.setMulticastInterface : Std.Async.UDP.Socket → Std.Net.IPAddr → IO Unit
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
/-- Given a morphism of simplicial sets `φ : A ⟶ B` with `A : X.Subcomplex` and
`B : Y.Subcomplex`, this is the type of morphisms `X ⟶ Y` which induce `φ`.  -/
SSet.RelativeMorphism : {X Y : SSet} → (A : X.Subcomplex) → (B : Y.Subcomplex) → (A.toSSet ⟶ B.toSSet) → Type u
-- Mathlib.Order.KrullDimension
Order.coheight_le_coe_iff : ∀ {α : Type u_1} [inst : Preorder α] {x : α} {n : ℕ}, Order.coheight x ≤ ↑n ↔ ∀ y > x, Order.coheight y < ↑n
-- Mathlib.Tactic.DeriveTraversable
/-- Run the following tactic:
```lean
intro _ .. x
dsimp only [Traversable.traverse, Functor.map]
induction x <;> (the simp tactic corresponding to s) <;> (tac)
```
 -/
Mathlib.Deriving.Traversable.traversableLawStarter : Lean.MVarId →
  Lean.Name →
    Lean.MetaM Lean.Meta.Simp.Context →
      (Array Lean.FVarId → Lean.Meta.InductionSubgoal → Lean.MVarId → Lean.MetaM Unit) → Lean.MetaM Unit
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.contract_rankFinite : ∀ {α : Type u_1} {M : Matroid α} {C : Set α} [M.RankFinite], (M.contract C).RankFinite
-- Mathlib.Data.UInt
/-- Is this an alphabetic ASCII character?  -/
UInt8.isASCIIAlpha : UInt8 → Bool
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.unop_op : ∀ {M : Type u_2} [inst : Add M] (S : AddSubsemigroup M), S.op.unop = S
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.StructuralAtom.leftUnitor.injEq : ∀ (e : Lean.Expr) (f : Mathlib.Tactic.BicategoryLike.Mor₁) (e_1 : Lean.Expr) (f_1 : Mathlib.Tactic.BicategoryLike.Mor₁),
  (Mathlib.Tactic.BicategoryLike.StructuralAtom.leftUnitor e f =
      Mathlib.Tactic.BicategoryLike.StructuralAtom.leftUnitor e_1 f_1) =
    (e = e_1 ∧ f = f_1)
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.eval₂_gcd_eq_zero : ∀ {R : Type u} {k : Type y} [inst : Field R] [inst_1 : CommSemiring k] [inst_2 : DecidableEq R] {ϕ : R →+* k}
  {f g : Polynomial R} {α : k},
  Polynomial.eval₂ ϕ α f = 0 → Polynomial.eval₂ ϕ α g = 0 → Polynomial.eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
-- Mathlib.Data.Nat.Multiplicity
Finset.Ico.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a b : α),
  Finset.Ico a b = LocallyFiniteOrder.finsetIco a b
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateCol_conjTranspose : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {b : n → α} [inst : DecidableEq m]
  [inst_1 : Star α], M.conjTranspose.updateCol i (star b) = (M.updateRow i b).conjTranspose
-- Init.Grind.Lemmas
Lean.Grind.Bool.or_eq_of_eq_true_right : ∀ {a b : Bool}, b = true → (a || b) = true
-- Std.Do.PredTrans
Std.Do.PredTrans.apply_bind : ∀ {ps : Std.Do.PostShape} {α β : Type u} (x : Std.Do.PredTrans ps α) (f : α → Std.Do.PredTrans ps β)
  (Q : Std.Do.PostCond β ps), (x.bind f).apply Q = x.apply (fun a => (f a).apply Q, Q.2)
-- Mathlib.Analysis.LocallyConvex.Bounded
/-- A complete space is quasi-complete with respect to any scalar ring.  -/
instQuasiCompleteSpaceOfCompleteSpace : ∀ {𝕜 : Type u_6} {E : Type u_7} [inst : Zero E] [inst_1 : UniformSpace E] [inst_2 : SeminormedRing 𝕜]
  [inst_3 : SMul 𝕜 E] [CompleteSpace E], QuasiCompleteSpace 𝕜 E
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₁ → (m₁ \ m₂).getKey? k = none
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preAleph_symm_natCast : ∀ (n : ℕ), Cardinal.preAleph.symm ↑n = ↑n
-- Mathlib.Algebra.Ring.Subring.Basic
RingHom.mem_eqLocus : ∀ {R : Type u} [inst : NonAssocRing R] {S : Type v} [inst_1 : Semiring S] {f g : R →+* S} {x : R},
  x ∈ f.eqLocus g ↔ f x = g x
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.ker_toSubmodule : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ),
  (Representation.IntertwiningMap.ker ρ σ f).toSubmodule = f.ker
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
/-- The product of localizations at all prime ideals of a commutative semiring.  -/
PrimeSpectrum.PiLocalization : (R : Type u_1) → [CommSemiring R] → Type u_1
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
ModelWithCorners.interior_disjointUnion : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {M' : Type u_5} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'],
  ModelWithCorners.interior (M ⊕ M') = Sum.inl '' ModelWithCorners.interior M ∪ Sum.inr '' ModelWithCorners.interior M'
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
balancedCore_eq_iInter : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {s : Set E}, 0 ∈ s → balancedCore 𝕜 s = ⋂ r, ⋂ (_ : 1 ≤ ‖r‖), r • s
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
SheafOfModules.freeFunctor_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {X Y : Type u} (f : X ⟶ Y),
  SheafOfModules.freeFunctor.map f = SheafOfModules.freeMap ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Topology.Order
setOfPred_isOpen_sup : ∀ {α : Type u} (t₁ t₂ : TopologicalSpace α), {s | IsOpen s} = {s | IsOpen s} ∩ {s | IsOpen s}
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- Negation on an additive group is an `AddEquiv` to the opposite group. When `G`
is commutative, there is `AddEquiv.inv`.  -/
AddEquiv.neg' : (G : Type u_3) → [inst : SubtractionMonoid G] → G ≃+ Gᵃᵒᵖ
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (x : CategoryTheory.Bicategory.Pith B),
  (CategoryTheory.Bicategory.Pith.inclusion B).obj x = x.as
-- Init.Data.List.OfFn
List.ofFnM_add : ∀ {k : ℕ} {α : Type u_1} {n : ℕ} {m : Type u_1 → Type u_2} [inst : Monad m] [LawfulMonad m] {f : Fin (n + k) → m α},
  List.ofFnM f = do
    let as ← List.ofFnM fun i => f (Fin.castLE ⋯ i)
    let bs ← List.ofFnM fun i => f (Fin.natAdd n i)
    pure (as ++ bs)
-- Mathlib.Data.Ordmap.Ordset
_private.Mathlib.Data.Ordmap.Ordset.0.Ordnode.Bounded.match_1.splitter : {α : Type u_1} →
  (motive : Ordnode α → WithBot α → WithTop α → Sort u_2) →
    (x : Ordnode α) →
      (x_1 : WithBot α) →
        (x_2 : WithTop α) →
          ((a b : α) → motive Ordnode.nil (some a) (some b)) →
            ((x : WithBot α) →
                (x_3 : WithTop α) → (∀ (a b : α), x = some a → x_3 = some b → False) → motive Ordnode.nil x x_3) →
              ((size : ℕ) →
                  (l : Ordnode α) →
                    (x : α) →
                      (r : Ordnode α) → (o₁ : WithBot α) → (o₂ : WithTop α) → motive (Ordnode.node size l x r) o₁ o₂) →
                motive x x_1 x_2
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.IsTotallyComplex.finrank : ∀ (K : Type u_2) [inst : Field K] [inst_1 : NumberField K] [h : NumberField.IsTotallyComplex K],
  Module.finrank ℚ K = 2 * NumberField.InfinitePlace.nrComplexPlaces K
-- Mathlib.Tactic.Linter.TextBased.UnicodeLinter
/-- Following any unicode character, this indicates that the text variant should be displayed  -/
Mathlib.Linter.TextBased.UnicodeLinter.UnicodeVariant.text : Char
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
/-- If `forget C` preserves initials and `X` is initial, then `ToType X` is empty.  -/
CategoryTheory.Limits.Concrete.empty_of_initial_of_preserves : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)] (X : C),
  Nonempty (CategoryTheory.Limits.IsInitial X) → IsEmpty (CategoryTheory.ToType X)
-- Mathlib.Order.Interval.Finset.Defs
Ioi_orderDual_def : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] (a : αᵒᵈ),
  Finset.Ioi a = Finset.map OrderDual.toDual.toEmbedding (Finset.Iio (OrderDual.ofDual a))
-- Init.Data.Nat.Lemmas
Nat.succ_eq_one_add : ∀ (n : ℕ), n.succ = 1 + n
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.isoMk_hom_s₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S}
  (s₀ : E.I₀ ≃ F.I₀) (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)) (s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j))
  (h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k))
  (w₀ :
    autoParam (∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i)
      CategoryTheory.PreOneHypercover.isoMk._auto_1)
  (w₁₁ :
    autoParam
      (∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁ k).hom (F.p₁ (s₁ k)) =
          CategoryTheory.CategoryStruct.comp (E.p₁ k) (h₀ i).hom)
      CategoryTheory.PreOneHypercover.isoMk._auto_3)
  (w₁₂ :
    autoParam
      (∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁ k).hom (F.p₂ (s₁ k)) =
          CategoryTheory.CategoryStruct.comp (E.p₂ k) (h₀ j).hom)
      CategoryTheory.PreOneHypercover.isoMk._auto_5)
  {i j : E.I₀} (k : E.I₁ i j), (CategoryTheory.PreOneHypercover.isoMk s₀ h₀ s₁ h₁ w₀ w₁₁ w₁₂).hom.s₁ k = s₁ k
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.injective_iff_isRegular : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S], Function.Injective ⇑(algebraMap R S) ↔ ∀ (c : ↥M), IsRegular ↑c
-- Mathlib.Order.Filter.FilterProduct
Filter.Germ.const_lt : ∀ {α : Type u} {β : Type v} {φ : Ultrafilter α} [inst : Preorder β] {x y : β}, x < y → ↑x < ↑y
-- Lean.Data.Array
/-- Inverse of `Array.mask`:
```
Array.zipMasked mask (Array.mask (mask.map not) xs) (Array.mask mask xs) == xs
```
 -/
Lean.Array.zipMasked : {α : Type} → Array Bool → Array α → Array α → Array α
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteGrp.instGroupCarrierToGrp.eq_1 : ∀ (G : FiniteGrp.{u_1}), G.instGroupCarrierToGrp = G.toGrp.str
-- Mathlib.Analysis.Calculus.FDeriv.Mul
fderiv_smul_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  {𝕜' : Type u_5} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F]
  [inst_8 : IsBoundedSMul 𝕜' F] [inst_9 : IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'},
  DifferentiableAt 𝕜 c x → ∀ (f : F), fderiv 𝕜 (fun y => c y • f) x = (fderiv 𝕜 c x).smulRight f
-- Mathlib.Topology.Algebra.Ring.Real
instIsTopologicalAddGroupReal : IsTopologicalAddGroup ℝ
-- Mathlib.Algebra.Order.SuccPred.PartialSups
partialSups_add_one : ∀ {α : Type u_1} {ι : Type u_2} [inst : SemilatticeSup α] [inst_1 : LinearOrder ι] [inst_2 : Add ι] [inst_3 : One ι]
  [inst_4 : LocallyFiniteOrderBot ι] [SuccAddOrder ι] (f : ι → α) (i : ι),
  (partialSups f) (i + 1) = (partialSups f) i ⊔ f (i + 1)
-- Mathlib.Topology.Homotopy.HSpaces
unitInterval.qRight_one_left : ∀ (θ : ↑unitInterval), unitInterval.qRight (1, θ) = 1
-- Aesop.Index.DiscrTreeConfig
Aesop.getMatch : {α : Type} → Lean.Meta.DiscrTree α → Lean.Expr → Lean.MetaM (Array α)
-- Mathlib.Order.Directed
/-- **Alias** of the reverse direction of `directedOn_iff_isCodirectedOrder`. -/
DirectedOn.of_isCodirectedOrder : ∀ {α : Type u_1} [inst : LE α] {s : Set α}, IsCodirectedOrder ↑s → DirectedOn (fun x1 x2 => x2 ≤ x1) s
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrableOn.mono_set : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} {s : Set X},
  MeasureTheory.LocallyIntegrableOn f s μ → ∀ {t : Set X}, t ⊆ s → MeasureTheory.LocallyIntegrableOn f t μ
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
/-- A subgroupoid `IsTotallyDisconnected` if it has only isotropy arrows.  -/
CategoryTheory.Subgroupoid.IsTotallyDisconnected : {C : Type u} → [inst : CategoryTheory.Groupoid C] → CategoryTheory.Subgroupoid C → Prop
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.map_vadd : ∀ {M : Type v} {α : Type w} {m : MeasurableSpace α} [inst : VAdd M α] [MeasurableConstVAdd M α] (c : M)
  (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure M α μ],
  MeasureTheory.Measure.map (fun x => c +ᵥ x) μ = μ
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` reflects limits of `K.op : Jᵒᵖ ⥤ Cᵒᵖ`, then `F : C ⥤ Dᵒᵖ` reflects
colimits of `K : J ⥤ C`.  -/
CategoryTheory.Limits.reflectsColimit_of_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C)
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.ReflectsLimit K.op F.leftOp],
  CategoryTheory.Limits.ReflectsColimit K F
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.pred_le_iff_le_succ : ∀ {a b : Ordinal.{u_4}}, a.pred ≤ b ↔ a ≤ Order.succ b
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Limits.IsColimit.mk.congr_simp : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F}
  (desc desc_1 : (s : CategoryTheory.Limits.Cocone F) → t.pt ⟶ s.pt) (e_desc : desc = desc_1)
  (fac :
    ∀ (s : CategoryTheory.Limits.Cocone F) (j : J), CategoryTheory.CategoryStruct.comp (t.ι.app j) (desc s) = s.ι.app j)
  (uniq :
    ∀ (s : CategoryTheory.Limits.Cocone F) (m : t.pt ⟶ s.pt),
      (∀ (j : J), CategoryTheory.CategoryStruct.comp (t.ι.app j) m = s.ι.app j) → m = desc s),
  { desc := desc, fac := fac, uniq := uniq } = { desc := desc_1, fac := ⋯, uniq := ⋯ }
-- Mathlib.Algebra.Order.CompleteField
/-- There is a unique ordered ring isomorphism between two conditionally complete linear ordered
fields.  -/
ConditionallyCompleteLinearOrderedField.uniqueOrderRingIso : (β : Type u_3) →
  (γ : Type u_4) →
    [inst : Field β] →
      [inst_1 : ConditionallyCompleteLinearOrder β] →
        [IsStrictOrderedRing β] →
          [inst_3 : Field γ] →
            [inst_4 : ConditionallyCompleteLinearOrder γ] → [IsStrictOrderedRing γ] → Unique (β ≃+*o γ)