mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanced_rotateR : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (ls : ℕ) (lk : α) (lv : β lk)
  (ll lr r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).Balanced →
    r.Balanced →
      Std.DTreeMap.Internal.Impl.BalanceLErasePrecond ls r.size ∨
          Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r.size ls →
        ls > Std.DTreeMap.Internal.delta * r.size → (Std.DTreeMap.Internal.Impl.rotateR k v lk lv ll lr r).Balanced
-- Init.Data.Array.Subarray.Split
/-- Keeps only the first `i` elements of the subarray. If there are `i` or fewer elements, the resulting
subarray is empty.
 -/
Subarray.take : {α : Type u_1} → Subarray α → ℕ → Subarray α
-- Mathlib.Algebra.GroupWithZero.Submonoid.CancelMulZero
/-- A submagma with zero of a cancellative magma with zero inherits cancellation.  -/
MulZeroMemClass.isCancelMulZero : ∀ {M₀ : Type u_1} [inst : Mul M₀] [inst_1 : Zero M₀] {S : Type u_2} [inst_2 : SetLike S M₀] [inst_3 : MulMemClass S M₀]
  [inst_4 : ZeroMemClass S M₀] (s : S) [IsCancelMulZero M₀], IsCancelMulZero ↥s
-- Mathlib.LinearAlgebra.Dimension.Constructions
rank_fin_fun : ∀ {R : Type u} [inst : Semiring R] [StrongRankCondition R] (n : ℕ), Module.rank R (Fin n → R) = ↑n
-- Mathlib.Order.Filter.Pointwise
/-- `pure` as an `AddMonoidHom`.  -/
Filter.pureAddMonoidHom : {α : Type u_2} → [inst : AddZeroClass α] → α →+ Filter α
-- Mathlib.Combinatorics.Graph.Delete
_private.Mathlib.Combinatorics.Graph.Delete.0.Graph.deleteVerts.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α), G.deleteVerts X = G.induce (G.vertexSet \ X)
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.enrichedHom_condition_assoc : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] {i j : J} (f : i ⟶ j) {Z : V}
  (h : (F₁.obj i ⟶[V] F₂.obj j) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.enrichedHomπ V F₁ F₂ i)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eHomWhiskerLeft V (F₁.obj i) (F₂.map f)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.enrichedHomπ V F₁ F₂ j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eHomWhiskerRight V (F₁.map f) (F₂.obj j)) h)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.sdiff_addFundamentalFrontier : ∀ (G : Type u_1) {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (s : Set α),
  s \ MeasureTheory.addFundamentalFrontier G s = MeasureTheory.addFundamentalInterior G s
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.trivialFibrations_eq_unop : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithFibrations C],
  HomotopicalAlgebra.trivialFibrations C = (HomotopicalAlgebra.trivialCofibrations Cᵒᵖ).unop
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsuppIsoLinear_apply : ∀ (R : Type u) [inst : Semiring R] (a : Polynomial R), (Polynomial.toFinsuppIsoLinear R) a = a.toFinsupp
-- Mathlib.Data.Stream.Init
Stream'.homomorphism : ∀ {α : Type u} {β : Type v} (f : α → β) (a : α), Stream'.pure f ⊛ Stream'.pure a = Stream'.pure (f a)
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
neg_one_lt_zero : ∀ {R : Type u} [inst : Ring R] [inst_1 : LinearOrder R] [ZeroLEOneClass R] [NeZero 1] [AddLeftStrictMono R], -1 < 0
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.instIsMonHomHomRightUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X : C} [inst_3 : CategoryTheory.MonObj X],
  CategoryTheory.IsMonHom (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
-- Mathlib.Data.DFinsupp.NeLocus
DFinsupp.nonempty_neLocus_iff : ∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst_1 : (a : α) → DecidableEq (N a)]
  [inst_2 : (a : α) → Zero (N a)] {f g : Π₀ (a : α), N a}, (f.neLocus g).Nonempty ↔ f ≠ g
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.instAdditiveOppositeFunctorAddCommGrpCatExtFunctor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (n : ℕ), (CategoryTheory.Abelian.extFunctor n).Additive
-- Mathlib.Data.Num.Bitwise
Num.instOrOp : OrOp Num
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Basic
TopRep.d_succ : ∀ {k : Type u_1} {G : Type u_2} [inst : Ring k] [inst_1 : Group G] [inst_2 : TopologicalSpace k]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] (X : TopRep k G) (n : ℕ),
  X.d (n + 1) = TopRep.ofHom (X.resolutionX (n + 1)).ρ.coind₁ι - (TopRep.coind₁Functor k G).map (X.d n)
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.const_apply : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : M) (g : R)
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (hu : ∀ x ∈ U, g ∈ x.asIdeal.primeCompl)
  (x : ↥U), ↑(AlgebraicGeometry.StructureSheaf.const f g U hu) x = LocalizedModule.mk f ⟨g, ⋯⟩
-- Mathlib.Control.Functor.Multivariate
TypeVec.append1.match_1.congr_eq_1 : ∀ {n : ℕ} (motive : Fin2 (n + 1) → Sort u_1) (x : Fin2 (n + 1)) (h_1 : (i : Fin2 n) → motive i.fs)
  (h_2 : Unit → motive Fin2.fz) (i : Fin2 n),
  x = i.fs →
    (match x with
      | i.fs => h_1 i
      | Fin2.fz => h_2 ()) ≍
      h_1 i
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_H : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C),
  (CategoryTheory.ShortComplex.RightHomologyData.ofAbelian S).H =
    CategoryTheory.Abelian.image
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.Limits.cokernel.π S.f))
-- Mathlib.Algebra.Group.Pi.Basic
Sum.elim_single_zero : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : Zero γ] (i : α)
  (c : γ), Sum.elim (Pi.single i c) 0 = Pi.single (Sum.inl i) c
-- Init.Data.Float.Float
instMulFloat : Mul Float
-- Lean.Meta.Tactic.SolveByElim
/-- Create or modify a `SolveByElimConfig` which rejects complete solutions for which `test`,
applied to the instantiations of the original goals, fails or returns `false`.
 -/
Lean.Meta.SolveByElim.SolveByElimConfig.testSolutions : optParam Lean.Meta.SolveByElim.SolveByElimConfig { } →
  (List Lean.Expr → Lean.MetaM Bool) → Lean.Meta.SolveByElim.SolveByElimConfig
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.UnitMonomial.isLittleO_of_lt : ∀ {basis : Tactic.ComputeAsymptotics.Basis} {m1 m2 : Tactic.ComputeAsymptotics.UnitMonomial},
  Tactic.ComputeAsymptotics.WellFormedBasis basis →
    List.length m1 = List.length basis →
      List.length m2 = List.length basis → m1 < m2 → m1.toFun basis =o[Filter.atTop] m2.toFun basis
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.lit.sizeOf_spec : ∀ (v : Lean.IR.LitVal), sizeOf (Lean.IR.Expr.lit v) = 1 + sizeOf v
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.WorkspaceClientCapabilities : Type
-- Mathlib.Algebra.Group.Defs
neg_eq_of_add_eq_zero_right : ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b : G}, a + b = 0 → -a = b
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.pushout_inl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {A B A' : C}
  (f : A ⟶ A') (g : A ⟶ B) [inst_1 : CategoryTheory.Limits.HasPushout f g] [P.IsStableUnderCobaseChangeAlong f],
  P g → P (CategoryTheory.Limits.pushout.inl f g)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.memLp_stoppedProcess_of_mem_finset : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Nonempty ι] {μ : MeasureTheory.Measure Ω}
  {τ : Ω → WithTop ι} {E : Type u_4} {p : ENNReal} {u : ι → Ω → E} [inst_1 : LinearOrder ι]
  [inst_2 : TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] {ℱ : MeasureTheory.Filtration ι m}
  [inst_5 : NormedAddCommGroup E],
  MeasureTheory.IsStoppingTime ℱ τ →
    (∀ (n : ι), MeasureTheory.MemLp (u n) p μ) →
      ∀ (n : ι) {s : Finset ι},
        (∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s) → MeasureTheory.MemLp (MeasureTheory.stoppedProcess u τ n) p μ
-- Mathlib.Topology.Algebra.Module.Equiv
/-- `ContinuousSemilinearEquivClass F σ M M₂` asserts `F` is a type of bundled continuous
`σ`-semilinear equivs `M → M₂`.  See also `ContinuousLinearEquivClass F R M M₂` for the case
where `σ` is the identity map on `R`.  A map `f` between an `R`-module and an `S`-module over a ring
homomorphism `σ : R →+* S` is semilinear if it satisfies the two properties `f (x + y) = f x + f y`
and `f (c • x) = (σ c) • f x`.  -/
ContinuousSemilinearEquivClass.map_continuous : ∀ {F : Type u_1} {R : outParam (Type u_2)} {S : outParam (Type u_3)} {inst : Semiring R} {inst_1 : Semiring S}
  {σ : outParam (R →+* S)} {σ' : outParam (S →+* R)} {inst_2 : RingHomInvPair σ σ'} {inst_3 : RingHomInvPair σ' σ}
  {M : outParam (Type u_4)} {inst_4 : TopologicalSpace M} {inst_5 : AddCommMonoid M} {M₂ : outParam (Type u_5)}
  {inst_6 : TopologicalSpace M₂} {inst_7 : AddCommMonoid M₂} {inst_8 : Module R M} {inst_9 : Module S M₂}
  {inst_10 : EquivLike F M M₂} [self : ContinuousSemilinearEquivClass F σ M M₂] (f : F), Continuous ⇑f
-- Mathlib.NumberTheory.NumberField.AdeleRing
NumberField.AdeleRing.algebraMap_injective : ∀ (R : Type u_1) (K : Type u_2) [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] [NumberField K],
  Function.Injective ⇑(algebraMap K (NumberField.AdeleRing R K))
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
CategoryTheory.ShortComplex.FunctorEquivalence.inverse_map_τ₂ : ∀ (J : Type u_1) (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)} (φ : X ⟶ Y),
  ((CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C).map φ).τ₂ =
    CategoryTheory.Functor.whiskerRight φ CategoryTheory.ShortComplex.π₂
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
/-- If the `p ^ n`th cyclotomic polynomial is irreducible, so is the `p ^ m`th, for `m ≤ n`.  -/
Polynomial.cyclotomic_irreducible_pow_of_irreducible_pow : ∀ {p : ℕ},
  Nat.Prime p →
    ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {n m : ℕ},
      m ≤ n → Irreducible (Polynomial.cyclotomic (p ^ n) R) → Irreducible (Polynomial.cyclotomic (p ^ m) R)
-- Mathlib.Data.Seq.Computation
_private.Mathlib.Data.Seq.Computation.0.Stream'.cons.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.image_symm_image_of_subset_target : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {s : Set β}, s ⊆ e.target → ↑e '' ↑e.symm '' s = s
-- Mathlib.Algebra.Group.Equiv.Defs
/-- Any type satisfying `AddEquivClass` can be cast into `AddEquiv` via
`AddEquivClass.toAddEquiv`.  -/
instCoeTCAddEquivOfAddEquivClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : EquivLike F α β] → [inst_1 : Add α] → [inst_2 : Add β] → [AddEquivClass F α β] → CoeTC F (α ≃+ β)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.maxView.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (l : Std.DTreeMap.Internal.Impl α β) →
      (motive :
          (r : Std.DTreeMap.Internal.Impl α β) →
            r.Balanced → Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size → Sort u_3) →
        (r : Std.DTreeMap.Internal.Impl α β) →
          (hr : r.Balanced) →
            (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size) →
              ((hr : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
                  (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size Std.DTreeMap.Internal.Impl.leaf.size) →
                    motive Std.DTreeMap.Internal.Impl.leaf hr hlr) →
                ((size : ℕ) →
                    (k' : α) →
                      (v' : β k') →
                        (l' r' : Std.DTreeMap.Internal.Impl α β) →
                          (hr : (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').Balanced) →
                            (hlr :
                                Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size
                                  (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').size) →
                              motive (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') hr hlr) →
                  motive r hr hlr
-- Aesop.Util.UnorderedArraySet
Aesop.UnorderedArraySet.partition : {α : Type u_1} →
  [inst : BEq α] → (α → Bool) → Aesop.UnorderedArraySet α → Aesop.UnorderedArraySet α × Aesop.UnorderedArraySet α
-- Lean.Compiler.LCNF.Basic
/-- Return the constructor names that have an explicit (non-default) alternative.
 -/
Lean.Compiler.LCNF.Cases.getCtorNames : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Cases pu → Lean.NameSet
-- Mathlib.Analysis.Analytic.Order
analyticOrderAt_mul_eq_top_of_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {f g : 𝕜 → 𝕜} {z₀ : 𝕜},
  analyticOrderAt g z₀ = ⊤ → analyticOrderAt (f * g) z₀ = ⊤
-- Mathlib.Data.Fintype.Order
Finite.ciInf_inf : ∀ {α : Type u_1} {ι : Type u_2} [Finite ι] [inst : ConditionallyCompleteLattice α] [Nonempty ι] {f : ι → α} {a : α},
  (⨅ i, f i) ⊓ a = ⨅ i, f i ⊓ a
-- Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
CliffordAlgebra.ofBaseChange_tmul_one : ∀ {R : Type u_1} (A : Type u_2) {V : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : AddCommGroup V]
  [inst_3 : Algebra R A] [inst_4 : Module R V] [inst_5 : Invertible 2] (Q : QuadraticForm R V) (z : A),
  (CliffordAlgebra.ofBaseChange A Q) (z ⊗ₜ[R] 1) = (algebraMap A (CliffordAlgebra (QuadraticForm.baseChange A Q))) z
-- Mathlib.Topology.Algebra.Valued.WithVal
/-- Type synonym for a ring equipped with the topology coming from a valuation.  -/
WithVal : {R : Type u_1} →
  {Γ₀ : Type u_2} → [inst : LinearOrderedCommGroupWithZero Γ₀] → [inst_1 : Ring R] → Valuation R Γ₀ → Type u_1
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- A special case of `f ∘ id = f`, `f` a Localization map.  -/
Submonoid.LocalizationMap.ofMulEquivOfDom_id : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N), f.ofMulEquivOfDom ⋯ = f
-- Init.Data.Int.Bitwise.Lemmas
Int.add_shiftLeft : ∀ (a b : ℤ) (n : ℕ), (a + b) <<< n = a <<< n + b <<< n
-- Mathlib.Order.InitialSeg
/-- The function in `collapse`.  -/
_private.Mathlib.Order.InitialSeg.0.collapseF : {α : Type u_1} →
  {β : Type u_2} →
    {r : α → α → Prop} → {s : β → β → Prop} → [IsWellOrder β s] → (f : r ↪r s) → (a : α) → { b // ¬s (f a) b }
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.coe_toAddSubgroup_symm_apply : ∀ {G : Type u_1} [inst : Group G] (S : AddSubgroup (Additive G)),
  ↑((RelIso.symm Subgroup.toAddSubgroup) S) = ⇑Multiplicative.toAdd ⁻¹' ↑S
-- Mathlib.Probability.Distributions.Uniform
PMF.ofMultiset_apply_of_notMem : ∀ {α : Type u_1} {s : Multiset α} (hs : s ≠ 0) {a : α}, a ∉ s → (PMF.ofMultiset s hs) a = 0
-- Mathlib.Topology.ContinuousMap.Polynomial
polynomialFunctions.starClosure_eq_adjoin_X : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : TopologicalSpace R] [inst_2 : IsTopologicalSemiring R]
  [inst_3 : StarRing R] [inst_4 : ContinuousStar R] (s : Set R),
  (polynomialFunctions s).starClosure = StarAlgebra.adjoin R {(Polynomial.toContinuousMapOnAlgHom s) Polynomial.X}
-- Mathlib.Topology.Algebra.Field
affineHomeomorph_image_Ioc : ∀ {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [inst_4 : IsTopologicalRing 𝕜] (a b c d : 𝕜) (h : 0 < a),
  ⇑(affineHomeomorph a b ⋯) '' Set.Ioc c d = Set.Ioc (a * c + b) (a * d + b)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_minKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {km fallback : α}, t.minKey? = some km → t.getKeyD km fallback = km
-- Init.Data.Int.DivMod.Lemmas
Int.emod_eq_add_self_emod : ∀ {a b : ℤ}, a % b = (a + b) % b
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.MutualMeasure.args.inj : ∀ {a a_1 : Array ℕ}, Lean.Elab.WF.GuessLex.MutualMeasure.args a = Lean.Elab.WF.GuessLex.MutualMeasure.args a_1 → a = a_1
-- Mathlib.Tactic.DuplicateDecls
/-- Structure used for sorting imported modules:
1. The number given by `libraryNumber`.
2. The name of the module as a string.
 -/
_private.Mathlib.Tactic.DuplicateDecls.0.Mathlib.Tactic.DuplicateDecls.ModuleKey : Type
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoid
/-- The inverse of an arrow in the free groupoid  -/
Quiver.FreeGroupoid.quotInv : {V : Type u} → [inst : Quiver V] → {X Y : Quiver.FreeGroupoid V} → (X ⟶ Y) → (Y ⟶ X)
-- Mathlib.Geometry.Manifold.Riemannian.Basic
/-- The emetric space structure associated to a Riemannian metric on a manifold. Designed
so that the topology is defeq to the original one.

This should only be used when constructing data in specific situations. To develop the theory,
one should rather assume that there is an already existing emetric space structure, which satisfies
additionally the predicate `IsRiemannianManifold I M`.  -/
EMetricSpace.ofRiemannianMetric : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {H : Type u_2} →
        [inst_2 : TopologicalSpace H] →
          (I : ModelWithCorners ℝ E H) →
            (M : Type u_3) →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : ChartedSpace H M] →
                  [inst_5 : Bundle.RiemannianBundle fun x => TangentSpace I x] →
                    [inst_6 : IsManifold I 1 M] →
                      [IsContinuousRiemannianBundle E fun x => TangentSpace I x] → [T3Space M] → EMetricSpace M
-- Init.Data.List.Attach
List.getElem_pmap : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p a → β) {l : List α} (h : ∀ a ∈ l, p a) {i : ℕ}
  (hn : i < (List.pmap f l h).length), (List.pmap f l h)[i] = f l[i] ⋯
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Impl.pruneLE.match_1.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.eq)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.lt with
    | Ordering.lt => h_1 ()
    | Ordering.eq => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_1 ()
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.cospanCompIso_inv_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z),
  (CategoryTheory.Limits.cospanCompIso F f g).inv.app CategoryTheory.Limits.WalkingCospan.left =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Limits.cospan (F.map f) (F.map g)).obj CategoryTheory.Limits.WalkingCospan.left)
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.ext_iff : ∀ {P : Type u_2} {inst : MetricSpace P} {x y : EuclideanGeometry.Sphere P},
  x = y ↔ x.center = y.center ∧ x.radius = y.radius
-- Mathlib.Algebra.Category.ModuleCat.Ulift
ModuleCat.instPreservesProjectiveObjectsUliftFunctorOfSmall : ∀ (R : Type u) [inst : Ring R] [Small.{v, u} R], (ModuleCat.uliftFunctor.{v', v, u} R).PreservesProjectiveObjects
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castSucc_Ioi : ∀ {n : ℕ} (i : Fin n), Fin.castSucc '' Set.Ioi i = Set.Ioo i.castSucc (Fin.last n)
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
/-- The canonical map from `ExteriorAlgebra R M` into `TrivSqZeroExt R M` that sends
`ExteriorAlgebra.ι` to `TrivSqZeroExt.inr`.  -/
ExteriorAlgebra.toTrivSqZeroExt : {R : Type u1} →
  [inst : CommRing R] →
    {M : Type u2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          [inst_3 : Module Rᵐᵒᵖ M] → [inst_4 : IsCentralScalar R M] → ExteriorAlgebra R M →ₐ[R] TrivSqZeroExt R M
-- Mathlib.Algebra.Order.Field.Basic
Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg : ∀ {α : Type u_4} [inst : GroupWithZero α] [inst_1 : PartialOrder α] {a b : α} [PosMulReflectLT α],
  0 < a → 0 ≤ b → 0 ≤ a / b
-- Mathlib.Combinatorics.Colex
/-- Strictly monotone functions preserve the colex ordering.  -/
Finset.Colex.toColex_image_le_toColex_image : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β} {s t : Finset α},
  StrictMono f → (toColex (Finset.image f s) ≤ toColex (Finset.image f t) ↔ toColex s ≤ toColex t)
-- Mathlib.LinearAlgebra.Dual.Defs
Submodule.comap_dualAnnihilator : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (Φ : Submodule R (Module.Dual R M)), Submodule.comap (Module.Dual.eval R M) Φ.dualAnnihilator = Φ.dualCoannihilator
-- Mathlib.Geometry.Manifold.DerivationBundle
/-- The derivations at a point of a manifold. Some regard this as a possible definition of the
tangent space, as this coincides with the usual tangent space for finite-dimensional `C^∞` real
manifolds. The identification is not true in general, though.  -/
PointDerivation : {𝕜 : 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] →
              ModelWithCorners 𝕜 E H →
                {M : Type u_4} → [inst : TopologicalSpace M] → [ChartedSpace H M] → M → Type (max (max u_4 u_1) u_1)
-- Mathlib.RingTheory.Extension.Presentation.Submersive
/-- If `algebraMap R S` is bijective, the empty generators are a pre-submersive
presentation with no relations.  -/
Algebra.PreSubmersivePresentation.ofBijectiveAlgebraMap : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          Function.Bijective ⇑(algebraMap R S) → Algebra.PreSubmersivePresentation R S PEmpty.{w + 1} PEmpty.{t + 1}
-- Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic
SimpleGraph.UnitDistEmbedding.subsingleton_p_apply : ∀ {V : Type u_1} (G : SimpleGraph V) {E : Type u_3} [inst : MetricSpace E] [inst_1 : Subsingleton V] (x : E) (x_1 : V),
  (SimpleGraph.UnitDistEmbedding.subsingleton G x).p x_1 = x
-- Init.Prelude
/-- The default maximum recursion depth. This is adjustable using the `maxRecDepth` option.  -/
Lean.defaultMaxRecDepth : ℕ
-- Mathlib.Order.CompleteLattice.Defs
lt_sSup_iff : ∀ {α : Type u_1} [inst : CompleteLinearOrder α] {s : Set α} {b : α}, b < sSup s ↔ ∃ a ∈ s, b < a
-- Init.Data.List.SplitOn.Basic
_private.Init.Data.List.SplitOn.Basic.0.List.splitOnPTR.go.eq_def : ∀ {α : Type u_1} (p : α → Bool) (a : List α) (a_1 : Array α) (a_2 : Array (List α)),
  List.splitOnPTR.go✝ p a a_1 a_2 =
    match a, a_1, a_2 with
    | [], acc, r => r.toListAppend [acc.toList]
    | a :: t, acc, r =>
      bif p a then List.splitOnPTR.go✝ p t #[] (r.push acc.toList) else List.splitOnPTR.go✝ p t (acc.push a) r
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
CategoryTheory.Adjunction.isLocalization_leftAdjoint : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁}
  [F.Full] [F.Faithful] (adj : G ⊣ F) (W : CategoryTheory.MorphismProperty C₁),
  W.IsInvertedBy G → W.functorCategory C₁ adj.unit → G.IsLocalization W