mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Vector.Extract
Vector.extract_extract : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i j k l : ℕ},
  (xs.extract i j).extract k l = Vector.cast ⋯ (xs.extract (i + k) (min (i + l) j))
-- Lean.Elab.Quotation
/-- Given the mapping `idxMap` built using `markRhss`, and `stx` the resulting syntax after expanding `match`-syntax,
return the pair `(stxNew, usedSet)`, where `stxNew` is `stx` after removing the `alt_idx` markers in `idxMap`,
and `i ∈ usedSet` if `stx` contains an `alt_idx` s.t. `alt_idx ↦ i` is in `idxMap`.
That is, `usedSet` contains the index of the used match-syntax right-hand-sides.
 -/
_private.Lean.Elab.Quotation.0.Lean.Elab.Term.Quotation.findUsedAlts : Lean.Syntax → Lean.NameMap ℕ → Lean.Elab.TermElabM (Lean.Syntax × Lean.Elab.Term.Quotation.IdxSet)
-- Mathlib.RingTheory.AdicCompletion.LocalRing
AdicCompletion.isMaximal_map_of_le : ∀ {R : Type u_1} [inst : CommRing R] (I m : Ideal R) [m.IsMaximal],
  I ≤ m → I.FG → (Ideal.map (algebraMap R (AdicCompletion I R)) m).IsMaximal
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.OpenNhdsOf.mk.injEq : ∀ {α : Type u_2} [inst : TopologicalSpace α] {x : α} (toOpens : TopologicalSpace.Opens α) (mem' : x ∈ toOpens.carrier)
  (toOpens_1 : TopologicalSpace.Opens α) (mem'_1 : x ∈ toOpens_1.carrier),
  ({ toOpens := toOpens, mem' := mem' } = { toOpens := toOpens_1, mem' := mem'_1 }) = (toOpens = toOpens_1)
-- Batteries.Data.String.Lemmas
String.utf8Len_le_of_prefix : ∀ {cs₁ cs₂ : List Char}, cs₁ <+: cs₂ → String.utf8Len cs₁ ≤ String.utf8Len cs₂
-- Batteries.Data.List.Basic
List.zipWithLeft.eq_2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (a : α) (as : List α),
  List.zipWithLeft f (a :: as) [] = List.map (fun a => f a none) (a :: as)
-- Init.Omega.Int
Lean.Omega.Int.add_nonneg_iff_neg_le' : ∀ {a b : ℤ}, 0 ≤ a + b ↔ -a ≤ b
-- Mathlib.Computability.ContextFreeGrammar
Language.IsContextFree.of_reverse : ∀ {T : Type u_1} {L : Language T}, L.reverse.IsContextFree → L.IsContextFree
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The right unitor isomorphism for binary coproducts with the initial object.  -/
CategoryTheory.Limits.coprod.rightUnitor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C] →
      [inst_2 : CategoryTheory.Limits.HasInitial C] → (P : C) → P ⨿ ⊥_ C ≅ P
-- Mathlib.Analysis.Distribution.DerivNotation
/-- The line derivative commutes with scalar multiplication, `∂_{v} (r • x) = r • ∂_{v} x` for all
`r : R` and `x : E`.
 -/
LineDerivSMul : (R : Type u_11) →
  (V : Type u) → (E : Type v) → (F : outParam (Type w)) → [SMul R E] → [SMul R F] → [LineDeriv V E F] → Prop
-- Mathlib.NumberTheory.Padics.MahlerBasis
/-- **Mahler's theorem**: for any continuous function `f` from `ℤ_[p]` to a `p`-adic Banach space, the
Mahler series with coefficients `n ↦ Δ_[1]^[n] f 0` converges to the original function `f`.
 -/
PadicInt.hasSum_mahler : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : Module ℤ_[p] E]
  [inst_2 : IsBoundedSMul ℤ_[p] E] [inst_3 : IsUltrametricDist E] [CompleteSpace E] (f : C(ℤ_[p], E)),
  HasSum (fun n => PadicInt.mahlerTerm ((fwdDiff 1)^[n] (⇑f) 0) n) f
-- Mathlib.LinearAlgebra.Pi
LinearMap.lsum_symm_apply : ∀ (R : Type u) {M : Type v} {ι : Type x} [inst : Semiring R] (φ : ι → Type i) [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : DecidableEq ι] (S : Type u_1) [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : Fintype ι] [inst_7 : Semiring S] [inst_8 : Module S M] [inst_9 : SMulCommClass R S M]
  (f : ((i : ι) → φ i) →ₗ[R] M) (i : ι), (LinearMap.lsum R φ S).symm f i = f ∘ₗ LinearMap.single R φ i
-- Mathlib.Topology.Homeomorph.Defs
Equiv.toHomeomorphOfIsInducing_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X ≃ Y)
  (hf : Topology.IsInducing ⇑f), ⇑(f.toHomeomorphOfIsInducing hf) = ⇑f
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
/-- For integrally closed domains, the minimal polynomial over the ring is the same as the minimal
polynomial over the fraction field. See `minpoly.isIntegrallyClosed_eq_field_fractions'` if
`S` is already a `K`-algebra.  -/
minpoly.isIntegrallyClosed_eq_field_fractions : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [IsDomain R] [inst_3 : Algebra R S]
  (K : Type u_3) (L : Type u_4) [inst_4 : Field K] [inst_5 : Algebra R K] [IsFractionRing R K] [inst_7 : CommRing L]
  [Nontrivial L] [inst_9 : Algebra R L] [inst_10 : Algebra S L] [inst_11 : Algebra K L] [IsScalarTower R K L]
  [IsScalarTower R S L] [IsIntegrallyClosed R] [IsDomain S] {s : S},
  IsIntegral R s → minpoly K ((algebraMap S L) s) = Polynomial.map (algebraMap R K) (minpoly R s)
-- Mathlib.Algebra.Central.TensorProduct
Algebra.IsCentral.left_of_tensor : ∀ (K : Type u_1) (B : Type u_2) (C : Type u_3) [inst : CommSemiring K] [inst_1 : Semiring B] [inst_2 : Semiring C]
  [inst_3 : Algebra K B] [inst_4 : Algebra K C],
  Function.Injective ⇑(algebraMap K C) →
    ∀ [Module.Flat K B] [hbc : Algebra.IsCentral K (TensorProduct K B C)], Algebra.IsCentral K B
-- Mathlib.Algebra.Order.Ring.Synonym
Lex.instRing : {R : Type u_1} → [Ring R] → Ring (Lex R)
-- Mathlib.RingTheory.Algebraic.MvPolynomial
MvPolynomial.transcendental_supported_X_iff : ∀ {σ : Type u_1} (R : Type u_2) [inst : CommRing R] [Nontrivial R] {i : σ} {s : Set σ},
  Transcendental (↥(MvPolynomial.supported R s)) (MvPolynomial.X i) ↔ i ∉ s
-- Mathlib.Algebra.Order.Group.Cone
GroupCone.oneLE.congr_simp : ∀ (H : Type u_1) [inst : CommGroup H] [inst_1 : PartialOrder H] [inst_2 : IsOrderedMonoid H],
  GroupCone.oneLE H = GroupCone.oneLE H
-- Mathlib.NumberTheory.Pell
/-- If `(x, y)` is a solution with `x` and `y` positive, then all its powers with positive
exponents have positive `y`.  -/
Pell.Solution₁.y_zpow_pos : ∀ {d : ℤ} {a : Pell.Solution₁ d}, 0 < a.x → 0 < a.y → ∀ {n : ℤ}, 0 < n → 0 < (a ^ n).y
-- Std.Sat.AIG.Basic
Std.Sat.AIG.CacheHit.mk.sizeOf_spec : ∀ {α : Type} {decls : Array (Std.Sat.AIG.Decl α)} {decl : Std.Sat.AIG.Decl α} [inst : SizeOf α] (idx : ℕ)
  (hbound : idx < decls.size) (hvalid : decls[idx] = decl),
  sizeOf { idx := idx, hbound := hbound, hvalid := hvalid } = 1 + sizeOf idx + sizeOf hbound + sizeOf hvalid
-- Lean.Expr
Lean.Literal.natVal.inj : ∀ {val val_1 : ℕ}, Lean.Literal.natVal val = Lean.Literal.natVal val_1 → val = val_1
-- Mathlib.GroupTheory.GroupAction.Quotient
MulActionHom.toQuotient_apply : ∀ {G : Type u} [inst : Group G] (H : Subgroup G) (g : G), (MulActionHom.toQuotient H) g = ↑g
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.truncTotal_eq_sum : ∀ {σ : Type u_1} {R : Type u_2} {n : ℕ} [inst : Finite σ] [inst_1 : CommSemiring R] (p : MvPowerSeries σ R),
  ↑((MvPowerSeries.truncTotal n) p) = ∑ i ∈ Finset.range n, (MvPowerSeries.homogeneousComponent i) p
-- Mathlib.MeasureTheory.OuterMeasure.Basic
MeasureTheory.measure_iUnion_le : ∀ {α : Type u_1} {ι : Type u_2} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α]
  {μ : F} [Countable ι] (s : ι → Set α), μ (⋃ i, s i) ≤ ∑' (i : ι), μ (s i)
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instAddSemigroup : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [AddSemigroup Y] → AddSemigroup (LocallyConstant X Y)
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Cauchy's **Mean Value Theorem**, `HasDerivAt` version.  -/
exists_ratio_hasDerivAt_eq_ratio_slope : ∀ (f f' : ℝ → ℝ) {a b : ℝ},
  a < b →
    ContinuousOn f (Set.Icc a b) →
      (∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x) →
        ∀ (g g' : ℝ → ℝ),
          ContinuousOn g (Set.Icc a b) →
            (∀ x ∈ Set.Ioo a b, HasDerivAt g (g' x) x) → ∃ c ∈ Set.Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c
-- Aesop.Tree.TreeM
Aesop.Tree.numGoals : Aesop.Tree → ℕ
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mk_injective : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] (s : Finset ι),
  Function.Injective (DFinsupp.mk s)
-- Init.Data.Array.Extract
Array.extract_eq_empty_of_le : ∀ {α : Type u_1} {j i : ℕ} {as : Array α}, min j as.size ≤ i → as.extract i j = #[]
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k k' : α},
      cmp k k' = Ordering.eq →
        ∀ {v fallback : β},
          List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l → (k, v) ∈ l → (t.insertMany l).getD k' fallback = v
-- Mathlib.MeasureTheory.Function.AEEqFun
/-- Coercion from a space of equivalence classes of almost everywhere strongly measurable
functions to functions. We ensure that if `f` has a constant representative,
then we choose that one.  -/
MeasureTheory.AEEqFun.cast : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] → {μ : MeasureTheory.Measure α} → [inst_1 : TopologicalSpace β] → (α →ₘ[μ] β) → α → β
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_inter!_eq_size_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      (∀ (a : α), Std.DTreeMap.Internal.Impl.contains a m₂ = true → Std.DTreeMap.Internal.Impl.contains a m₁ = true) →
        (m₁.inter! m₂).size = m₂.size
-- Init.Data.List.Lemmas
List.getElem?_insert_zero : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List α} {a : α},
  (List.insert a l)[0]? = if a ∈ l then l[0]? else some a
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- The map from the (any as stated) initial object to any other object is a
monomorphism  -/
CategoryTheory.Limits.InitialMonoClass.isInitial_mono_from : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} [self : CategoryTheory.Limits.InitialMonoClass C] {I : C}
  (X : C) (hI : CategoryTheory.Limits.IsInitial I), CategoryTheory.Mono (hI.to X)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imK_im : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [inst : Zero R], a.im.imK = a.imK
-- Init.Data.Fin.Lemmas
Fin.le_total : ∀ {n : ℕ} (a b : Fin n), a ≤ b ∨ b ≤ a
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalOpposite.mopFunctor_η : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.mopFunctor C) =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.mopFunctor C).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey?_erase_eq_iff_not_compare_eq_maxKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.erase k).maxKey? = t.maxKey? ↔ ∀ {km : α}, t.maxKey? = some km → ¬cmp k km = Ordering.eq
-- Mathlib.Algebra.Ring.Defs
CommRing.toCommMonoid : {α : Type u} → [self : CommRing α] → CommMonoid α
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Ring.inverse_mul_cancel : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] (x : M₀), IsUnit x → Ring.inverse x * x = 1
-- Mathlib.LinearAlgebra.Dimension.Localization
IsLocalizedModule.rank_eq : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  ∀ p ≤ nonZeroDivisors R,
    ∀ {N : Type uM} [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M →ₗ[R] N) [IsLocalizedModule p f],
      Module.rank R N = Module.rank R M
-- Mathlib.NumberTheory.Real.GoldenRatio
/-- **Binet's formula** as a dependent equality.  -/
Real.coe_fib_eq : ∀ (n : ℕ), ↑(Nat.fib n) = (Real.goldenRatio ^ n - Real.goldenConj ^ n) / √5
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.FiniteSpanningSetsIn.finite : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {C : Set (Set α)}
  (self : μ.FiniteSpanningSetsIn C) (i : ℕ), μ (self.set i) < ⊤
-- Mathlib.Data.Finset.Union
Finset.disjiUnion_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Finset α} {t : α → Finset β} {f : β ↪ γ}
  {h : (↑s).PairwiseDisjoint t}, Finset.map f (s.disjiUnion t h) = s.disjiUnion (fun a => Finset.map f (t a)) ⋯
-- Lean.Data.Options
Lean.getOptionDescr : Lean.Name → IO String
-- Mathlib.CategoryTheory.Square
/-- The composition of morphisms of squares.  -/
CategoryTheory.Square.Hom.comp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {sq₁ sq₂ sq₃ : CategoryTheory.Square C} → sq₁.Hom sq₂ → sq₂.Hom sq₃ → sq₁.Hom sq₃
-- Lean.Hygiene
Lean.sanitizeSyntax : Lean.Syntax → StateM Lean.NameSanitizerState Lean.Syntax
-- Init.Data.Range.Polymorphic.UInt
UInt32.instLeast? : Std.PRange.Least? UInt32
-- Mathlib.Data.Set.Basic
set_coe_cast : ∀ {α : Type u} {s t : Set α} (H' : s = t) (H : ↑s = ↑t) (x : ↑s), cast H x = ⟨↑x, ⋯⟩
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.map_coord_zero : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] (f : M [⋀^ι]→L[R] N) {m : ι → M} (i : ι), m i = 0 → f m = 0
-- Init.Data.String.PosRaw
/-- Returns the size of the byte slice delineated by the positions `lo` and `hi`.
 -/
String.Pos.Raw.byteDistance : String.Pos.Raw → String.Pos.Raw → ℕ
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.final_fromPUnit_of_isTerminal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {c : C} (hc : CategoryTheory.Limits.IsTerminal c),
  (CategoryTheory.Functor.fromPUnit c).Final
-- Lean.Data.Lsp.TextSync
Lean.Lsp.DidCloseTextDocumentParams.textDocument : Lean.Lsp.DidCloseTextDocumentParams → Lean.Lsp.TextDocumentIdentifier
-- Mathlib.CategoryTheory.Category.Preorder
CategoryTheory.le_of_op_hom : ∀ {X : Type u} [inst : Preorder X] {x y : Xᵒᵖ} (h : x ⟶ y), Opposite.unop y ≤ Opposite.unop x
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
SimplyConnectedSpace.instPathConnectedSpace : ∀ {X : Type u_3} [inst : TopologicalSpace X] [SimplyConnectedSpace X], PathConnectedSpace X
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙL_apply : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {a : A} (ha : p a)
  (a_1 : ContinuousMapZero (↑(quasispectrum R a)) R), (cfcₙL ha) a_1 = (cfcₙHom ha) a_1
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesOnBall.analyticAt : ∀ {𝕜 : 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] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal}, HasFPowerSeriesOnBall f p x r → AnalyticAt 𝕜 f x
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- A compactly coherent space that is Hausdorff is compactly generated.  -/
of_compactlyCoherentSpace_of_t2 : ∀ {X : Type u} [inst : TopologicalSpace X] [T2Space X] [CompactlyCoherentSpace X], CompactlyGeneratedSpace X
-- Mathlib.Dynamics.OmegaLimit
/-- The ω-limit of a set `s` under `ϕ` with respect to a filter `f` is `⋂ u ∈ f, cl (ϕ u s)`.  -/
omegaLimit : {τ : Type u_1} → {α : Type u_2} → {β : Type u_3} → [TopologicalSpace β] → Filter τ → (τ → α → β) → Set α → Set β
-- Mathlib.LinearAlgebra.Eigenspace.Zero
LinearMap.charpoly_constantCoeff_eq_zero_iff : ∀ {K : Type u_2} {M : Type u_3} [inst : Field K] [inst_1 : AddCommGroup M] [inst_2 : Module K M]
  [inst_3 : Module.Finite K M] (φ : Module.End K M),
  Polynomial.constantCoeff (LinearMap.charpoly φ) = 0 ↔ ∃ m, m ≠ 0 ∧ φ m = 0
-- Lean.Meta.DiscrTree.Main
_private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.toNatLit?.loop : Lean.Expr → OptionT Id ℕ
-- Lean.Language.Basic
/-- Syntax to be inspected for reuse.  -/
Lean.Language.SyntaxGuarded.stx : {α : Type} → Lean.Language.SyntaxGuarded α → Lean.Syntax
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.leComap_id_iff : ∀ {X : Type u_2} [inst : TopologicalSpace X] {A A' : DiscreteQuotient X},
  DiscreteQuotient.LEComap (ContinuousMap.id X) A A' ↔ A ≤ A'
-- Lean.Widget.InteractiveDiagnostic
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.msgToInteractiveAux : Lean.MessageData → IO (Std.Format × Array Lean.Widget.EmbedFmt✝)
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.add_nat_le_add_nat_iff : ∀ {α β : Cardinal.{u_1}} (n : ℕ), α + ↑n ≤ β + ↑n ↔ α ≤ β
-- Mathlib.Tactic.Order
/-- Core of the `order` tactic.  -/
Mathlib.Tactic.Order.orderCore : Bool → Array Lean.Expr → Lean.Expr → Lean.MVarId → Lean.MetaM Unit
-- Mathlib.Analysis.CStarAlgebra.Fuglede
/-- The map `expMulMulExp : ℂ → A` given by `z ↦ exp (z • star b) * x * exp (z • star (-a))` for
fixed `a b x : A`.  -/
_private.Mathlib.Analysis.CStarAlgebra.Fuglede.0.expMulMulExp : {A : Type u_1} → [CStarAlgebra A] → A → A → A → ℂ → A
-- Mathlib.Data.Subtype
Function.extend.eq_1 : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) (g : α → γ) (j : β → γ) (b : β),
  Function.extend f g j b = if h : ∃ a, f a = b then g (Classical.choose h) else j b
-- Mathlib.Order.Filter.Finite
/-- **Alias** of `Set.Finite.eventuallyEq_iUnion`. -/
Filter.EventuallyEq.biUnion : ∀ {α : Type u} {l : Filter α} {ι : Type u_2} {s : Set ι},
  s.Finite → ∀ {f g : ι → Set α}, (∀ i ∈ s, f i =ᶠ[l] g i) → ⋃ i ∈ s, f i =ᶠ[l] ⋃ i ∈ s, g i
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.mk : {Γ : Type u_8} →
  {R : Type u_9} →
    [inst : PartialOrder Γ] →
      [inst_1 : AddCommMonoid R] →
        {α : Type u_7} →
          (toFun : α → HahnSeries Γ R) →
            (⋃ a, (toFun a).support).IsPWO →
              (∀ (g : Γ), {a | (toFun a).coeff g ≠ 0}.Finite) → HahnSeries.SummableFamily Γ R α
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.SolverExtension.mk.inj : ∀ {σ : Type} {id : ℕ} {mkInitial : IO σ} {internalize : Lean.Expr → Option Lean.Expr → Lean.Meta.Grind.GoalM Unit}
  {newEq newDiseq : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit} {mbtc : Lean.Meta.Grind.GoalM Bool}
  {action : Lean.Meta.Grind.Action} {check : Lean.Meta.Grind.GoalM Bool} {checkInv : Lean.Meta.Grind.GoalM Unit}
  {id_1 : ℕ} {mkInitial_1 : IO σ} {internalize_1 : Lean.Expr → Option Lean.Expr → Lean.Meta.Grind.GoalM Unit}
  {newEq_1 newDiseq_1 : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit} {mbtc_1 : Lean.Meta.Grind.GoalM Bool}
  {action_1 : Lean.Meta.Grind.Action} {check_1 : Lean.Meta.Grind.GoalM Bool} {checkInv_1 : Lean.Meta.Grind.GoalM Unit},
  { id := id, mkInitial := mkInitial, internalize := internalize, newEq := newEq, newDiseq := newDiseq, mbtc := mbtc,
        action := action, check := check, checkInv := checkInv } =
      { id := id_1, mkInitial := mkInitial_1, internalize := internalize_1, newEq := newEq_1, newDiseq := newDiseq_1,
        mbtc := mbtc_1, action := action_1, check := check_1, checkInv := checkInv_1 } →
    id = id_1 ∧
      mkInitial = mkInitial_1 ∧
        internalize = internalize_1 ∧
          newEq = newEq_1 ∧
            newDiseq = newDiseq_1 ∧ mbtc = mbtc_1 ∧ action = action_1 ∧ check = check_1 ∧ checkInv = checkInv_1
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
AddChar.zmod_injective : ∀ {n : ℕ} [inst : NeZero n], Function.Injective (AddChar.zmod n)
-- Init.Data.Nat.Lemmas
Nat.min_add_right_self : ∀ {a b : ℕ}, min a (a + b) = a
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.toSubtype.eq_1 : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  (p : J → Prop) [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)],
  CategoryTheory.Limits.biproduct.toSubtype f p =
    CategoryTheory.Limits.biproduct.lift fun x => CategoryTheory.Limits.biproduct.π f ↑x
-- Mathlib.Algebra.Group.End
Equiv.Perm.one_symm : ∀ {α : Type u_4}, Equiv.symm 1 = 1
-- Lean.Language.Lean.Types
Lean.Language.Lean.instToSnapshotTreeCommandElaboratingSnapshot : Lean.Language.ToSnapshotTree Lean.Language.Lean.CommandElaboratingSnapshot
-- Mathlib.Topology.Homotopy.Lifting
/-- Unique characterization of the lifted path.  -/
IsCoveringMap.eq_liftPath_iff' : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X}
  (cov : IsCoveringMap p) {γ : C(↑unitInterval, X)} {e : E} (γ_0 : γ 0 = p e) {Γ : C(↑unitInterval, E)},
  Γ = cov.liftPath γ e γ_0 ↔ p ∘ ⇑Γ = ⇑γ ∧ Γ 0 = e
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
/-- The cofork constructed in `coequalizerCofork` is indeed a colimit cocone.  -/
AlgebraicGeometry.LocallyRingedSpace.coequalizerCoforkIsColimit : {X Y : AlgebraicGeometry.LocallyRingedSpace} →
  (f g : X ⟶ Y) → CategoryTheory.Limits.IsColimit (AlgebraicGeometry.LocallyRingedSpace.coequalizerCofork f g)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.whiskerRight_μ_δ_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X Y : C) (T : D) {Z : D}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) T ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.LaxMonoidal.μ F X Y) T)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.δ F X Y) T) h) =
    h
-- Mathlib.Algebra.Order.Positive.Ring
Positive.val_one : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R], ↑1 = 1
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.lcompₛₗ_apply : ∀ {R : Type u_14} {R₂ : Type u_15} {R₃ : Type u_16} {R₅ : Type u_18} {M : Type u_19} {N : Type u_20} {P : Type u_21}
  [inst : Semiring R] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : Semiring R₅] {σ₁₂ : R →+* R₂}
  {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P]
  [inst_7 : Module R M] [inst_8 : Module R₂ N] [inst_9 : Module R₃ P] [inst_10 : Module R₅ P]
  [inst_11 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_12 : SMulCommClass R₃ R₅ P] (f : M →ₛₗ[σ₁₂] N) (g : N →ₛₗ[σ₂₃] P)
  (x : M), ((LinearMap.lcompₛₗ R₅ P σ₂₃ f) g) x = g (f x)
-- Init.Data.SInt.Bitwise
instLawfulCommIdentityISizeHXorOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 ^^^ x2) 0
-- Mathlib.Data.Finset.Defs
/-- Convert a finset to a set in the natural way.  -/
Finset.instSetLike : {α : Type u_1} → SetLike (Finset α) α
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_X₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z), (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).L₃.X₃ = CategoryTheory.Limits.cokernel g
-- Mathlib.Algebra.Group.Defs
CommGroup.toGroup : {G : Type u} → [self : CommGroup G] → Group G
-- Mathlib.CategoryTheory.Galois.Decomposition
_private.Mathlib.CategoryTheory.Galois.Decomposition.0.CategoryTheory.PreGaloisCategory.mkSelfProdFib_map_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C)
  (t : (F.obj X).obj),
  (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.Limits.Pi.π (fun x => X) t)))
      (CategoryTheory.PreGaloisCategory.mkSelfProdFib✝ F X) =
    t