mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- The composition of a `C^n` function on a domain with a `C^n` function is `C^n`.  -/
ContDiff.comp_contDiffOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {s : Set E} {g : F → G} {f : E → F},
  ContDiff 𝕜 n g → ContDiffOn 𝕜 n f s → ContDiffOn 𝕜 n (g ∘ f) s
-- Mathlib.LinearAlgebra.Prod
LinearMap.inr_map_mul : ∀ {R : Type u} [inst : Semiring R] {A : Type u_4} [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  {B : Type u_5} [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] (b₁ b₂ : B),
  (LinearMap.inr R A B) (b₁ * b₂) = (LinearMap.inr R A B) b₁ * (LinearMap.inr R A B) b₂
-- Mathlib.Data.Int.CardIntervalMod
/-- There are `⌊b / r⌋ - ⌊a / r⌋` multiples of `r` in `(a, b]`, if `a ≤ b`.  -/
Int.Ioc_filter_dvd_card : ∀ (a b : ℤ) {r : ℤ}, 0 < r → ↑{x ∈ Finset.Ioc a b | r ∣ x}.card = max (⌊↑b / ↑r⌋ - ⌊↑a / ↑r⌋) 0
-- Mathlib.Data.PFun
PFun.preimage_subset_dom : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β), f.preimage s ⊆ f.Dom
-- Mathlib.Algebra.Ring.Defs
/-- An associative but not-necessarily unital semiring.  -/
NonUnitalSemiring : Type u → Type u
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) (x : List ((a : α) × β a)),
  Std.Internal.List.getValueCast? a x =
    match x with
    | [] => none
    | ⟨k, v⟩ :: l => if h : (k == a) = true then some (cast ⋯ v) else Std.Internal.List.getValueCast? a l
-- Mathlib.Data.Set.Basic
Set.inter_nonempty : ∀ {α : Type u} {s t : Set α}, (s ∩ t).Nonempty ↔ ∃ x ∈ s, x ∈ t
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- A variant of `hasBasis_nhds` where `· ≠ 0` is unbundled.  -/
IsValuativeTopology.hasBasis_nhds' : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] [inst_2 : TopologicalSpace R] [IsValuativeTopology R]
  (x : R), (nhds x).HasBasis (fun x => x ≠ 0) fun x_1 => {y | (ValuativeRel.valuation R) (y - x) < x_1}
-- Lean.Elab.Tactic.Try
/-- Returns tactic for `evalAndSuggest` (unsafe version that can evaluate user generators)  -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.mkTryEvalSuggestStxUnsafe : Lean.MVarId → Lean.Meta.Try.Info → Lean.MetaM (Lean.TSyntax `tactic)
-- Batteries.Data.List.Lemmas
List.replaceFTR.go.match_1.congr_eq_2 : ∀ {α : Type u_1} (motive : List α → Array α → Sort u_2) (x : List α) (x_1 : Array α)
  (h_1 : (acc : Array α) → motive [] acc) (h_2 : (x : α) → (xs : List α) → (acc : Array α) → motive (x :: xs) acc)
  (x_2 : α) (xs : List α) (acc : Array α),
  x = x_2 :: xs →
    x_1 = acc →
      (match x, x_1 with
        | [], acc => h_1 acc
        | x :: xs, acc => h_2 x xs acc) ≍
        h_2 x_2 xs acc
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.symm_apply : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  (F : f₀.Homotopy f₁) (x : ↑unitInterval × X), F.symm x = F (unitInterval.symm x.1, x.2)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.copyBase_Indep : ∀ {α : Type u_1} (M : Matroid α) (E : Set α) (IsBase : Set α → Prop) (hE : E = M.E)
  (h : ∀ (B : Set α), IsBase B ↔ M.IsBase B) (a : Set α), (M.copyBase E IsBase hE h).Indep a = M.Indep a
-- Mathlib.Combinatorics.Matroid.Map
Matroid.comap_indep_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {I : Set α} {N : Matroid β},
  (N.comap f).Indep I ↔ N.Indep (f '' I) ∧ Set.InjOn f I
-- Mathlib.AlgebraicGeometry.Cover.Over
AlgebraicGeometry.Scheme.instOverPullbackCoverOverProp' : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  (S : AlgebraicGeometry.Scheme) →
    [inst : P.IsStableUnderBaseChange] →
      [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] →
        {X W : AlgebraicGeometry.Scheme} →
          (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) →
            (f : W ⟶ X) →
              [inst_2 : W.Over S] →
                [inst_3 : X.Over S] →
                  [inst_4 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰] →
                    [inst_5 : AlgebraicGeometry.Scheme.Hom.IsOver f S] →
                      {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
                        [inst_6 : Q.HasOfPostcompProperty Q] →
                          [inst_7 : Q.IsStableUnderBaseChange] →
                            [inst_8 : Q.IsStableUnderComposition] →
                              (hX : Q (X ↘ S)) →
                                (hW : Q (W ↘ S)) →
                                  (hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)) →
                                    AlgebraicGeometry.Scheme.Cover.Over S
                                      (AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp' S 𝒰 f hX hW hQ)
-- Mathlib.Data.Finset.Functor
/-- Traverse function for `Finset`.  -/
Finset.traverse : {α β : Type u} →
  {F : Type u → Type u} →
    [inst : Applicative F] → [CommApplicative F] → [DecidableEq β] → (α → F β) → Finset α → F (Finset β)
-- Mathlib.Data.Set.Finite.Basic
/-- This is a kind of induction principle. See `Finset.induction` for the usual induction principle
for finsets.  -/
Finset.forall : ∀ {α : Type u} {p : Finset α → Prop}, (∀ (s : Finset α), p s) ↔ ∀ (s : Set α) (hs : s.Finite), p hs.toFinset
-- Aesop.Forward.PremiseIndex
Aesop.instHashablePremiseIndex : Hashable Aesop.PremiseIndex
-- Mathlib.Tactic.Widget.Calc
CalcParams.toSelectInsertParams : CalcParams → SelectInsertParams
-- Init.Data.Format.Basic
Std.Format.instBEqFlattenBehavior.beq : Std.Format.FlattenBehavior → Std.Format.FlattenBehavior → Bool
-- Mathlib.Algebra.Order.Group.Action.Synonym
Lex.instAddAction : {M : Type u_1} → {α : Type u_3} → [inst : AddMonoid M] → [AddAction M α] → AddAction (Lex M) α
-- Mathlib.AlgebraicGeometry.Limits
/-- (Implementation Detail)
The coproduct of the two schemes is given by indexed coproducts over `WalkingPair`.  -/
AlgebraicGeometry.coprodIsoSigma : (X Y : AlgebraicGeometry.Scheme) → X ⨿ Y ≅ ∐ fun i => CategoryTheory.Limits.WalkingPair.casesOn i.down X Y
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
upperHemicontinuous_singleton_id : ∀ {α : Type u_1} [inst : TopologicalSpace α], UpperHemicontinuous fun x => {x}
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.infNatTrans_app : ∀ (k : Type u) {G : Type u} [inst : CommRing k] [inst_1 : Group G] (S : Subgroup G) [inst_2 : S.Normal] (n : ℕ)
  (A : Rep.{u, u, u} k G),
  (groupCohomology.infNatTrans k S n).app A =
    groupCohomology.map (QuotientGroup.mk' S) (Rep.ofHom (A.ρ.quotientToInvariants_lift S)) n
-- Mathlib.GroupTheory.Nilpotent
/-- The lower central series of an additive group is a descending central series.  -/
AddSubgroup.lowerCentralSeries_isDescendingCentralSeries : ∀ {G : Type u_1} [inst : AddGroup G], AddSubgroup.IsDescendingCentralSeries ⊤.lowerCentralSeries
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.mapA.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
-- Mathlib.Order.Notation
/-- Heyting implication `⇨` 

Conventions for notations in identifiers:

 * The recommended spelling of `⇨` in identifiers is `himp`. -/
HImp.himp : {α : Type u_1} → [self : HImp α] → α → α → α
-- Mathlib.Probability.Decision.Risk.Basic
ProbabilityTheory.bayesRisk_const_of_neZero : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal},
  Measurable (Function.uncurry ℓ) →
    ∀ (μ : MeasureTheory.Measure 𝓧) [NeZero μ] [MeasureTheory.IsFiniteMeasure μ] (π : MeasureTheory.Measure Θ)
      [MeasureTheory.SFinite π],
      ProbabilityTheory.bayesRisk ℓ (ProbabilityTheory.Kernel.const Θ μ) π = ⨅ y, ∫⁻ (θ : Θ), ℓ θ y * μ Set.univ ∂π
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.leadingCoeff_eq : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : Zero Γ] {x : HahnSeries Γ R},
  x.leadingCoeff = x.coeff x.order
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork_K : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (c : CategoryTheory.Limits.KernelFork S.g)
  (hc : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork S hf c hc).K = c.pt
-- Mathlib.Order.Filter.Basic
Filter.Eventually.congr : ∀ {α : Type u} {f : Filter α} {p q : α → Prop},
  (∀ᶠ (x : α) in f, p x) → (∀ᶠ (x : α) in f, p x ↔ q x) → ∀ᶠ (x : α) in f, q x
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.cardSupp_neg : ∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : AddGroup R] (x : HahnSeries Γ R),
  (-x).cardSupp = x.cardSupp
-- Mathlib.Algebra.Homology.HomotopyFiber
HomologicalComplex.pathObject.mapHomologicalComplexObjIso_inv_map_π₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {α : Type u_2}
  {c : ComplexShape α} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasPathObject]
  {D : Type u_3} [inst_5 : CategoryTheory.Category.{v_2, u_3} D] [inst_6 : CategoryTheory.Preadditive D]
  (H : CategoryTheory.Functor C D) [inst_7 : H.Additive]
  [inst_8 :
    ∀ (i : α),
      CategoryTheory.Limits.HasBinaryBiproduct (((H.mapHomologicalComplex c).obj K).X i)
        (((H.mapHomologicalComplex c).obj K).X i)]
  [inst_9 : ((H.mapHomologicalComplex c).obj K).HasPathObject]
  [inst_10 :
    ∀ (i : α),
      CategoryTheory.Limits.HasBinaryBiproduct (((H.op.mapHomologicalComplex c.symm).obj K.op).X i)
        (((H.op.mapHomologicalComplex c.symm).obj K.op).X i)]
  [inst_11 :
    HomologicalComplex.HasHomotopyCofiber
      (CategoryTheory.Limits.biprod.lift
        (CategoryTheory.CategoryStruct.id ((H.op.mapHomologicalComplex c.symm).obj K.op))
        (-CategoryTheory.CategoryStruct.id ((H.op.mapHomologicalComplex c.symm).obj K.op)))]
  [inst_12 :
    HomologicalComplex.HasHomotopyCofiber
      ((H.op.mapHomologicalComplex c.symm).map
        (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K.op)
          (-CategoryTheory.CategoryStruct.id K.op)))]
  [inst_13 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.op.X i) (K.op.X i)]
  (hc : ∀ (i : α), ∃ j, c.Rel i j),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.pathObject.mapHomologicalComplexObjIso K H hc).inv
      ((H.mapHomologicalComplex c).map (HomologicalComplex.pathObject.π₁ K)) =
    HomologicalComplex.pathObject.π₁ ((H.mapHomologicalComplex c).obj K)
-- Lean.Elab.PreDefinition.PartialFixpoint.Eqns
Lean.Elab.PartialFixpoint.registerEqnsInfo : Array Lean.Elab.PreDefinition →
  Lean.Name → Lean.Elab.FixedParamPerms → Array Lean.Elab.PartialFixpointType → Lean.MetaM Unit
-- Std.Http.Data.Status
/-- 415 Unsupported Media Type
 -/
Std.Http.Status.unsupportedMediaType : Std.Http.Status
-- Mathlib.Data.Num.Lemmas
PosNum.cast_add : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] (m n : PosNum), ↑(m + n) = ↑m + ↑n
-- Mathlib.Topology.Separation.Hausdorff
eq_of_nhds_neBot : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] {x y : X}, (nhds x ⊓ nhds y).NeBot → x = y
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.coe_toContinuousLinearMap : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (e : A →A[R] B), ⇑e.toContinuousLinearMap = ⇑e
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, k ∈ t.insert k v
-- Mathlib.RingTheory.Congruence.Defs
RingCon.toCon_coe_eq_coe : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] (c : RingCon R), ⇑c.toCon = ⇑c
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsMaximumIndepSet.maximum : ∀ {α : Type u_3} [inst : Finite α] {G : SimpleGraph α} {s : Finset α},
  G.IsMaximumIndepSet s → ∀ (t : Finset α), G.IsIndepSet ↑t → t.card ≤ s.card
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_le_iff : ∀ {x y : ℝ}, √x ≤ y ↔ 0 ≤ y ∧ x ≤ y ^ 2
-- Lean.Meta.Tactic.Grind.Action
Lean.Meta.Grind.Action.saveStateIfTracing : Lean.Meta.Grind.GrindM (Option Lean.Meta.Grind.SavedState)
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.pow_ne_top : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MonoidWithZero α] [inst_2 : NoZeroDivisors α] [inst_3 : Nontrivial α]
  {x : WithTop α} {n : ℕ}, x ≠ ⊤ → x ^ n ≠ ⊤
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesOnBall.eventually_eq_zero : ∀ {𝕜 : 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} {x : E}
  {r : ENNReal}, HasFPowerSeriesOnBall f 0 x r → ∀ᶠ (z : E) in nhds x, f z = 0
-- Mathlib.Analysis.CStarAlgebra.Basic
CStarRing.norm_one : ∀ {E : Type u_2} [inst : NormedRing E] [inst_1 : StarRing E] [CStarRing E] [Nontrivial E], ‖1‖ = 1
-- Mathlib.Topology.Bases
TopologicalSpace.Subtype.firstCountableTopology : ∀ {α : Type u} [t : TopologicalSpace α] (s : Set α) [FirstCountableTopology α], FirstCountableTopology ↑s
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.map_pure : ∀ {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {α β : Type w} {f : α → β} {a : α},
  Std.Iterators.PostconditionT.map f (pure a) = pure (f a)
-- Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
_private.Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas.0.ZMod.eisenstein_lemma_aux₁ : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] [hp2 : Fact (p % 2 = 1)] {a : ℕ},
  ↑a ≠ 0 →
    ↑(∑ x ∈ Finset.Ico 1 (p / 2).succ, a * x) =
      ↑{x ∈ Finset.Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val}.card + ↑(∑ x ∈ Finset.Ico 1 (p / 2).succ, x) +
        ↑(∑ x ∈ Finset.Ico 1 (p / 2).succ, a * x / p)
-- Lean.Message
/-- Structured message data. We use it for reporting errors, trace messages, etc.  -/
Lean.MessageData : Type
-- Mathlib.Analysis.Convex.Topology
/-- The closed interior of a simplex is a closed set.  -/
Affine.Simplex.isClosed_closedInterior : ∀ {𝕜 : Type u_4} {V : Type u_5} {P : Type u_6} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderClosedTopology 𝕜] [CompactIccSpace 𝕜] [ContinuousAdd 𝕜] [inst_7 : AddCommGroup V]
  [inst_8 : TopologicalSpace V] [IsTopologicalAddGroup V] [inst_10 : Module 𝕜 V] [ContinuousSMul 𝕜 V]
  [inst_12 : AddTorsor V P] [inst_13 : TopologicalSpace P] [IsTopologicalAddTorsor P] [T2Space P] {n : ℕ}
  (s : Affine.Simplex 𝕜 P n), IsClosed s.closedInterior
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.floor.eq_1 : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E) [inst_3 : LinearOrder K] [inst_4 : IsStrictOrderedRing K]
  [inst_5 : FloorRing K] [inst_6 : Fintype ι] (m : E),
  ZSpan.floor b m = ∑ i, ⌊(b.repr m) i⌋ • (Module.Basis.restrictScalars ℤ b) i
-- Mathlib.Analysis.Normed.Group.Basic
dist_one_right : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a : E), dist a 1 = ‖a‖
-- Mathlib.Algebra.Group.Prod
MulEquiv.prodUnique_symm_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : Unique N] (a : M),
  MulEquiv.prodUnique.symm a = (a, default)
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.restrictScalars_add : ∀ {R : Type u_14} {S : Type u_15} {M : Type u_16} {N : Type u_17} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module S M] [inst_7 : Module S N] [inst_8 : LinearMap.CompatibleSMul M N R S] (f g : M →ₗ[S] N),
  ↑R (f + g) = ↑R f + ↑R g
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.diff_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {t₃ : Std.TreeSet.Raw α cmp},
  t₁.WF → t₂.WF → t₃.WF → t₂.Equiv t₃ → (t₁ \ t₂).Equiv (t₁ \ t₃)
-- Mathlib.Data.Set.Function
Set.InjOn.of_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {f : α → β} {g : β → γ}, Set.InjOn (g ∘ f) s → Set.InjOn f s
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernel.mapIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {X' Y' : C} (f' : X' ⟶ Y')
  [inst_3 : CategoryTheory.Limits.HasKernel f'] (p : X ≅ X') (q : Y ≅ Y')
  (w : CategoryTheory.CategoryStruct.comp f q.hom = CategoryTheory.CategoryStruct.comp p.hom f'),
  (CategoryTheory.Limits.kernel.mapIso f f' p q w).inv = CategoryTheory.Limits.kernel.map f' f p.inv q.inv ⋯
-- Init.Data.Slice.Array.Lemmas
Array.stop_toSubarray : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ}, (xs.toSubarray lo hi).stop = min hi xs.size
-- Init.Data.Array.Find
Array.findIdx?_eq_bind_find?_idxOf? : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {xs : Array α} {p : α → Bool},
  Array.findIdx? p xs = (Array.find? p xs).bind fun x => xs.idxOf? x
-- Mathlib.LinearAlgebra.Finsupp.Defs
/-- Interpret `Finsupp.mapDomain` as a linear map.  -/
Finsupp.lmapDomain : {α : Type u_1} →
  (M : Type u_2) →
    (R : Type u_5) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → {α' : Type u_9} → (α → α') → (α →₀ M) →ₗ[R] α' →₀ M
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α} [inst_1 : Inhabited (β k)], (m₁ ∪ m₂).get! k = m₂.getD k (m₁.get! k)
-- Mathlib.MeasureTheory.Constructions.Projective
MeasureTheory.IsProjectiveLimit.measure_univ_eq : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)]
  {P : (J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)} {μ : MeasureTheory.Measure ((i : ι) → α i)},
  MeasureTheory.IsProjectiveLimit μ P → ∀ (I : Finset ι), μ Set.univ = (P I) Set.univ
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.toNormalizedChainComplexNatTrans_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (R : C) (X : SSet),
  (SSet.toNormalizedChainComplexNatTrans R).app X = X.toNormalizedChainComplex R
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g] {Z_1 : C} (h : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f g).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g f) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
/-- If `f` is a transfinite composition of shape `J`, then it is
also a transfinite composition of shape `J'` if `J' ≃o J`.  -/
CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          {X Y : C} →
            {f : X ⟶ Y} →
              [inst_3 : SuccOrder J] →
                [inst_4 : WellFoundedLT J] →
                  CategoryTheory.TransfiniteCompositionOfShape J f →
                    {J' : Type w'} →
                      [inst_5 : LinearOrder J'] →
                        [inst_6 : OrderBot J'] →
                          [inst_7 : SuccOrder J'] →
                            [inst_8 : WellFoundedLT J'] → J' ≃o J → CategoryTheory.TransfiniteCompositionOfShape J' f
-- Mathlib.Topology.Separation.SeparatedNhds
SeparatedNhds.mono : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s₁ s₂ t₁ t₂ : Set X},
  SeparatedNhds s₂ t₂ → s₁ ⊆ s₂ → t₁ ⊆ t₂ → SeparatedNhds s₁ t₁
-- Mathlib.Data.NNReal.Defs
NNReal.sub_def : ∀ {r p : NNReal}, r - p = (↑r - ↑p).toNNReal
-- Mathlib.Data.Vector.Basic
/-- The `tail` of a vector made up of one element is `nil`.  -/
List.Vector.singleton_tail : ∀ {α : Type u_1} (v : List.Vector α 1), v.tail = List.Vector.nil
-- Mathlib.LinearAlgebra.Matrix.Action
Matrix.instSMulCommClassForall_1 : ∀ {n : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : DistribSMul S R] [SMulCommClass S R R], SMulCommClass S (Matrix n n R) (n → R)
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.closure_finite_subsets : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s : Set α), closure {K | (↑K).Finite ∧ ↑K ⊆ s} = {K | ↑K ⊆ closure s}
-- Mathlib.Control.Combinators
/-- Executes `tm` or `fm` depending on whether the result of `mbool` is `true` or `false`
respectively.  -/
condM : {m : Type → Type} → [Monad m] → {α : Type} → m Bool → m α → m α → m α
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.totalDegree_expand : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {p : ℕ} (f : MvPolynomial σ R),
  ((MvPolynomial.expand p) f).totalDegree = f.totalDegree * p
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.isCentralScalar : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : SMulZeroClass N R]
  [inst_2 : SMulZeroClass Nᵐᵒᵖ R] [IsCentralScalar N R], IsCentralScalar N (AddMonoidAlgebra R M)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
/-- The Fourier transform of line derivative in direction `m` is given by multiplication of
`(2 * π * Complex.I) • (inner ℝ · m)` with the Fourier transform.  -/
SchwartzMap.fourier_lineDerivOp_eq : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_3} [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MeasurableSpace V] [inst_6 : BorelSpace V]
  (f : SchwartzMap V E) (m : V),
  FourierTransform.fourier (LineDeriv.lineDerivOp m f) =
    (2 * ↑Real.pi * Complex.I) • (SchwartzMap.smulLeftCLM E fun x => inner ℝ x m) (FourierTransform.fourier f)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.sigmaToPiHomeo_apply : ∀ {ι : Type u_1} {R : ι → Type u_2} [inst : (i : ι) → CommRing (R i)] [inst_1 : Finite ι]
  (p : (i : ι) × PrimeSpectrum (R i)), (PrimeSpectrum.sigmaToPiHomeo R) p = PrimeSpectrum.sigmaToPi R p
-- Mathlib.Data.FP.Basic
FP.Float.inf.injEq : ∀ [C : FP.FloatCfg] (a a_1 : Bool), (FP.Float.inf a = FP.Float.inf a_1) = (a = a_1)
-- Mathlib.Algebra.Free
FreeAddMagma.lift_symm_apply : ∀ {α : Type u} {β : Type v} [inst : Add β] (F : FreeAddMagma α →ₙ+ β) (a : α),
  FreeAddMagma.lift.symm F a = (⇑F ∘ FreeAddMagma.of) a
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
SymmetricAlgebra.lift_ι_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] (f : M →ₗ[R] A) (a : M),
  (SymmetricAlgebra.lift f) ((SymmetricAlgebra.ι R M) a) = f a
-- Mathlib.LinearAlgebra.Dimension.RankNullity
exists_set_linearIndependent : ∀ (R : Type u_1) (M : Type u) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [HasRankNullity.{u, u_1} R], ∃ s, Cardinal.mk ↑s = Module.rank R M ∧ LinearIndependent (ι := ↑s) R Subtype.val
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly.eq_10 : ∀ (k : ℕ) (n : ℤ),
  ((Lean.Grind.CommRing.Expr.intCast n).pow k).toPoly =
    bif k == 0 then Lean.Grind.CommRing.Poly.num 1 else Lean.Grind.CommRing.Poly.num (n ^ k)