mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Prod
LieHom.snd_surjective : ∀ {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂], Function.Surjective ⇑(LieHom.snd R L₁ L₂)
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.map_update_sub : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommGroup N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [inst_7 : DecidableEq ι] (m : ι → M) (i : ι) (x y : M),
  f (Function.update m i (x - y)) = f (Function.update m i x) - f (Function.update m i y)
-- Mathlib.GroupTheory.Archimedean
/-- Given a subgroup `H` of a decidable linearly ordered mul-archimedean abelian group `G`, if there
exists a minimal element `a` of `H ∩ G_{>1}` then `H` is generated by `a`.  -/
Subgroup.cyclic_of_min : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {H : Subgroup G}
  {a : G}, IsLeast {g | g ∈ H ∧ 1 < g} a → H = Subgroup.closure {a}
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.span_range_inclusionSpan : ∀ {R : Type u_1} {M : Type u_4} (S : Type u_7) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Semiring S] [inst_4 : SMul R S] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] (p : Submodule R M),
  Submodule.span S (Set.range ⇑(Submodule.inclusionSpan S p)) = ⊤
-- Mathlib.Data.Set.MulAntidiagonal
Set.AddAntidiagonal.finite_of_isWF : ∀ {α : Type u_1} [inst : AddCancelCommMonoid α] [inst_1 : LinearOrder α] [AddLeftMono α] [AddRightStrictMono α]
  {s t : Set α}, s.IsWF → t.IsWF → ∀ (a : α), (s.antidiagonal t a).Finite
-- Mathlib.Data.List.Infix
List.inits_reverse : ∀ {α : Type u_1} (l : List α), l.reverse.inits = (List.map List.reverse l.tails).reverse
-- Mathlib.Data.List.Defs
/-- Quaternary version of `list.zipWith`.  -/
List.zipWith4 : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} → {δ : Type u_4} → {ε : Type u_5} → (α → β → γ → δ → ε) → List α → List β → List γ → List δ → List ε
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
/-- We can characterize elements in an admissible list as exactly those for which
`simplicialEvalσ` takes the same value twice in a row.  -/
SimplexCategoryGenRel.mem_isAdmissible_iff : ∀ {m : ℕ} (L : List ℕ),
  SimplexCategoryGenRel.IsAdmissible m L →
    ∀ (j : ℕ),
      j ∈ L ↔
        j < m + L.length ∧ SimplexCategoryGenRel.simplicialEvalσ L j = SimplexCategoryGenRel.simplicialEvalσ L (j + 1)
-- Batteries.Util.Cache
/-- Function for adding a declaration from the current file to the cache.  -/
Batteries.Tactic.DeclCache.addDecl : {α : Type} → Batteries.Tactic.DeclCache α → Lean.Name → Lean.ConstantInfo → α → Lean.MetaM α
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.mk : {B : Type u_1} → {M : CoxeterMatrix B} → {W : Type u_2} → [inst : Group W] → W ≃* M.Group → CoxeterSystem M W
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- If `f' : ℂ → E` is a derivative of a complex differentiable function on the circle
`Metric.sphere c |R|`, then `∮ z in C(c, R), f' z = 0`.  -/
circleIntegral.integral_eq_zero_of_hasDerivWithinAt' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f f' : ℂ → E} {c : ℂ}
  {R : ℝ},
  (∀ z ∈ Metric.sphere c |R|, HasDerivWithinAt f (f' z) (Metric.sphere c |R|) z) → ∮ (z : ℂ) in C(c, R), f' z = 0
-- Mathlib.Algebra.Group.Equiv.Defs
/-- `e.symm` is a right inverse of `e`, written as `e (e.symm y) = y`.  -/
MulEquiv.apply_symm_apply : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N) (y : N), e (e.symm y) = y
-- Mathlib.Order.Cover
Pi.exists_forall_antisymmRel_of_covBy : ∀ {ι : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → Preorder (α i)] {a b : (i : ι) → α i},
  a ⋖ b → ∃ i, ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 => x1 ≤ x2) (a j) (b j)
-- Init.System.IO
/-- Runs a process to completion and captures its output and exit code.
The child process is run with a null standard input or the specified input if provided,
and the current process blocks until it has run to completion.

The specifications of standard input, output, and error handles in `args` are ignored.
 -/
IO.Process.output : IO.Process.SpawnArgs → optParam (Option String) none → IO IO.Process.Output
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_eq_neg_pi_div_two : ∀ {x : ℝ}, Real.arcsin x = -(Real.pi / 2) ↔ x ≤ -1
-- Mathlib.CategoryTheory.Limits.FinallySmall
CategoryTheory.instFinallySmallOppositeOfInitiallySmall : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] [CategoryTheory.InitiallySmall J],
  CategoryTheory.FinallySmall Jᵒᵖ
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift.0.Std.Iterators.Types.ULiftIterator.Monadic.modifyStep.match_1.eq_1 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3)
  (it' : Std.IterM m β) (out : β) (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Mathlib.SetTheory.Cardinal.Basic
/-- **Alias** of `Cardinal.exists_ne_ne_of_three_le`. -/
Cardinal.three_le : ∀ {α : Type u_1}, 3 ≤ Cardinal.mk α → ∀ (x y : α), ∃ z, z ≠ x ∧ z ≠ y
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Complex.Gamma_ofReal : ∀ (s : ℝ), Complex.Gamma ↑s = ↑(Real.Gamma s)
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.IsCircuit.eRk_add_one_eq : ∀ {α : Type u_1} {M : Matroid α} {C : Set α}, M.IsCircuit C → M.eRk C + 1 = C.encard
-- Lean.Data.Lsp.Basic
Lean.Lsp.CreateFile.instFromJsonOptions.fromJson : Lean.Json → Except String Lean.Lsp.CreateFile.Options
-- Mathlib.Analysis.Convex.Segment
lineMap_mem_segment : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [AddRightMono 𝕜] [inst_3 : AddCommGroup E]
  [inst_4 : Module 𝕜 E] (a b : E) {t : 𝕜}, t ∈ Set.Icc 0 1 → (AffineMap.lineMap a b) t ∈ segment 𝕜 a b
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
/-- The function `Real.cos` is real analytic.  -/
Real.analyticAt_cos : ∀ {x : ℝ}, AnalyticAt ℝ Real.cos x
-- Aesop.Saturate
Aesop.SaturateM.Context.mk : Aesop.Options' → Aesop.SaturateM.Context
-- Mathlib.Order.Category.PartOrdEmb
partOrdEmb_dual_comp_forget_to_pardOrd : PartOrdEmb.dual.comp (CategoryTheory.forget₂ PartOrdEmb PartOrd) =
  (CategoryTheory.forget₂ PartOrdEmb PartOrd).comp PartOrd.dual
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- **Alias** of `Left.mul_le_one`.

---

Assumes left covariance.
The lemma assuming right covariance is `Right.mul_le_one`.  -/
mul_le_one' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftMono α] {a b : α}, a ≤ 1 → b ≤ 1 → a * b ≤ 1
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.WhiskerRight.whisker.injEq : ∀ (e : Mathlib.Tactic.BicategoryLike.Mor₂) (η : Mathlib.Tactic.BicategoryLike.WhiskerRight)
  (f : Mathlib.Tactic.BicategoryLike.Atom₁) (e_1 : Mathlib.Tactic.BicategoryLike.Mor₂)
  (η_1 : Mathlib.Tactic.BicategoryLike.WhiskerRight) (f_1 : Mathlib.Tactic.BicategoryLike.Atom₁),
  (Mathlib.Tactic.BicategoryLike.WhiskerRight.whisker e η f =
      Mathlib.Tactic.BicategoryLike.WhiskerRight.whisker e_1 η_1 f_1) =
    (e = e_1 ∧ η = η_1 ∧ f = f_1)
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.floor_add_natCast : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R}
  [IsStrictOrderedRing R], 0 ≤ a → ∀ (n : ℕ), ⌊a + ↑n⌋₊ = ⌊a⌋₊ + n
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.add_not : ∀ {w : ℕ} (a : BitVec w), a + ~~~a = -1#w
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.subset_compl_comm : ∀ {α : Type u_1} {s t : Finset α} [inst : Fintype α] [inst_1 : DecidableEq α], s ⊆ tᶜ ↔ t ⊆ sᶜ
-- Mathlib.LinearAlgebra.TensorPower.Basic
TensorPower.mul_algebraMap₀ : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ} (r : R)
  (a : TensorPower R n M), (TensorPower.cast R M ⋯) (GradedMonoid.GMul.mul a (TensorPower.algebraMap₀ r)) = r • a
-- Init.Omega.Constraint
Lean.Omega.Constraint.mk : Lean.Omega.LowerBound → Lean.Omega.UpperBound → Lean.Omega.Constraint
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.diff_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ m₃ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m₂.Equiv m₃ → (m₁ \ m₂).Equiv (m₁ \ m₃)
-- Mathlib.Topology.Algebra.Monoid.Defs
Filter.Tendsto.add : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M] [ContinuousAdd M] {α : Type u_2} {f g : α → M}
  {x : Filter α} {a b : M},
  Filter.Tendsto f x (nhds a) → Filter.Tendsto g x (nhds b) → Filter.Tendsto (fun x => f x + g x) x (nhds (a + b))
-- Init.Grind.Interactive
Lean.Parser.Tactic.Grind.«grind_filterGen≥_» : Lean.ParserDescr
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- `Finset α` is an `AddSemigroup` under pointwise operations if `α` is.  -/
Finset.addSemigroup : {α : Type u_2} → [DecidableEq α] → [AddSemigroup α] → AddSemigroup (Finset α)
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- The `decompose'` argument of `weightedDecomposition`.  -/
MvPolynomial.decompose' : (R : Type u_1) →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      {σ : Type u_3} →
        (w : σ → M) →
          [inst_1 : AddCommMonoid M] →
            [DecidableEq M] → MvPolynomial σ R → DirectSum M fun i => ↥(MvPolynomial.weightedHomogeneousSubmodule R w i)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α} [inst_2 : Inhabited β],
  (List.map Prod.fst l).contains k = false → (t.insertMany l)[k]! = t[k]!
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.instDiscreteTopology : ∀ {M : Type u_1} [inst : TopologicalSpace M] [DiscreteTopology M], DiscreteTopology Mᵈᵐᵃ
-- Lean.Parser.Term
/-- `+generalize` directs `let`/`have` to generalize the value from the expected type before elaborating the body.
 -/
Lean.Parser.Term.letOptGeneralize : Lean.Parser.Parser
-- Batteries.Recycling.MonadSatisfying.Basic
/-- If `p` is always true, then every `x` satisfies it.
(This is the strongest postcondition version of `of_true`.)
 -/
SatisfiesM.trivial : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Functor m] [LawfulFunctor m] {x : m α}, SatisfiesM (fun x => True) x
-- Mathlib.Topology.Algebra.Monoid
continuousAdd_iInf : ∀ {M : Type u_3} {ι' : Sort u_6} [inst : Add M] {ts : ι' → TopologicalSpace M},
  (∀ (i : ι'), ContinuousAdd M) → ContinuousAdd M
-- Std.Time.Date.Unit.Month
Std.Time.Month.instLTOffset : LT Std.Time.Month.Offset
-- Mathlib.Probability.Kernel.CondDistrib
MeasureTheory.AEStronglyMeasurable.ae_integrable_condDistrib_map_iff : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] [inst_3 : NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F},
  AEMeasurable Y μ →
    MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ) →
      ((∀ᵐ (a : β) ∂MeasureTheory.Measure.map X μ,
            MeasureTheory.Integrable (fun ω => f (a, ω)) ((ProbabilityTheory.condDistrib Y X μ) a)) ∧
          MeasureTheory.Integrable (fun a => ∫ (ω : Ω), ‖f (a, ω)‖ ∂(ProbabilityTheory.condDistrib Y X μ) a)
            (MeasureTheory.Measure.map X μ) ↔
        MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ))
-- Mathlib.LinearAlgebra.SymplecticGroup
SymplecticGroup.map_mem : ∀ {l : Type u_1} {R : Type u_2} [inst : DecidableEq l] [inst_1 : Fintype l] [inst_2 : CommRing R]
  {A : Matrix (l ⊕ l) (l ⊕ l) R} {F : Type u_3} {S : Type u_4} [inst_3 : CommRing S] [inst_4 : FunLike F R S]
  [RingHomClass F R S], A ∈ Matrix.symplecticGroup l R → ∀ (f : F), A.map ⇑f ∈ Matrix.symplecticGroup l S
-- Mathlib.LinearAlgebra.Prod
/-- Graph of a linear map.  -/
LinearMap.graph : {R : Type u} →
  {M : Type v} →
    {M₂ : Type w} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid M₂] →
            [inst_3 : Module R M] → [inst_4 : Module R M₂] → (M →ₗ[R] M₂) → Submodule R (M × M₂)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [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 → Std.ExtDHashMap.Const.getD (Std.ExtDHashMap.Const.insertMany m l) k' fallback = v
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.get_eq_getₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.OrientedOrd α] [inst_2 : Std.LawfulEqOrd α] (k : α)
  (l : Std.DTreeMap.Internal.Impl α β) {h : k ∈ l} (h' : (l.get?ₘ k).isSome = true), l.get k h = l.getₘ k h'
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.DecreasingBy.mk : Lean.Syntax → Lean.TSyntax `Lean.Parser.Tactic.tacticSeq → Lean.Elab.DecreasingBy
-- Mathlib.RingTheory.LittleWedderburn
/-- A finite division ring is a field. See `Finite.isDomain_to_isField` and
`Fintype.divisionRingOfIsDomain` for more general statements, but these create data, and therefore
may cause diamonds if used improperly.  -/
littleWedderburn : (D : Type u_1) → [DivisionRing D] → [Finite D] → Field D
-- Mathlib.Analysis.Distribution.TemperateGrowth
Function.HasTemperateGrowth.pow : ∀ {R : Type u_3} {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedRing R]
  [inst_3 : NormedAlgebra ℝ R] {f : E → R},
  Function.HasTemperateGrowth f → ∀ (k : ℕ), Function.HasTemperateGrowth (f ^ k)
-- Mathlib.Topology.MetricSpace.Kuratowski
/-- A function `f : α → ℓ^∞(ι, ℝ)` which is `K`-Lipschitz on a subset `s` admits a `K`-Lipschitz
extension to the whole space.

Theorem 2.2 of [Assaf Naor, *Metric Embeddings and Lipschitz Extensions*][Naor-2015]

The same result for the case of a finite type `ι` is implemented in
`LipschitzOnWith.extend_pi`.
 -/
LipschitzOnWith.extend_lp_infty : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {ι : Type u_1} {f : α → ↥(lp (fun x => ℝ) ⊤)} {K : NNReal},
  LipschitzOnWith K f s → ∃ g, LipschitzWith K g ∧ Set.EqOn f g s
-- Mathlib.Algebra.Order.Group.Action.Synonym
Lex.instIsScalarTower : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : SMul M N] [inst_1 : SMul M α] [inst_2 : SMul N α]
  [IsScalarTower M N α], IsScalarTower (Lex M) N α
-- Mathlib.Topology.Path
Path.symm_symm : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ : Path x y), γ.symm.symm = γ
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomotopyInvariance
/-- If `f` and `g` are homotopic maps of simplicial sets, then they induce chain-homotopic
maps on the singular chain complexes with coefficients in `R`.
 -/
SSet.Homotopy.chainComplexMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasCoproducts C] →
        {X Y : SSet} →
          {f g : X ⟶ Y} → SSet.Homotopy f g → (R : C) → Homotopy (SSet.chainComplexMap f R) (SSet.chainComplexMap g R)
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.subst_add : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S},
  MvPowerSeries.HasSubst a →
    ∀ (f g : MvPowerSeries σ R), MvPowerSeries.subst a (f + g) = MvPowerSeries.subst a f + MvPowerSeries.subst a g
-- Mathlib.Data.Finsupp.SMul
Finsupp.smul_single_one : ∀ {α : Type u_1} {R : Type u_6} [inst : MulZeroOneClass R] (a : α) (b : R), (b • fun₀ | a => 1) = fun₀ | a => b
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- If `i = i'` and `j = j'` this is an equivalence between the `1`-index type at `i`, `j` and
the one at `i'`, `j'`.  -/
CategoryTheory.PreOneHypercover.congrIndexOneOfEq : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} → {E : CategoryTheory.PreOneHypercover S} → {i i' j j' : E.I₀} → i = i' → j = j' → E.I₁ i j ≃ E.I₁ i' j'
-- Mathlib.NumberTheory.Padics.PadicNorm
/-- The `p`-adic norm respects division.  -/
padicNorm.div : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (q r : ℚ), padicNorm p (q / r) = padicNorm p q / padicNorm p r
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instAddMonoid.eq_1 : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] [inst_2 : ContinuousAdd M],
  SeparationQuotient.instAddMonoid =
    { toAddSemigroup := SeparationQuotient.instAddSemigroup, toZero := SeparationQuotient.instZero, zero_add := ⋯,
      add_zero := ⋯, toNSMul := NSMul.ofSMul, nsmul_zero := ⋯, nsmul_succ := ⋯ }
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.exists_nat_gt_of_mk_nonneg : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R] {x : R},
  0 ≤ ArchimedeanClass.mk x → ∃ n, x < ↑n
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
/-- Given a simplicial set `X`, the cokernel of the differential `d 1 0`
of the chain complex of `X` with coefficients in `R` identifies
to the coproduct of copies of `R` indexed by `π₀ X`.  -/
SSet.isColimitCokernelCoforkChainComplexDOneZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        (X : SSet) →
          (R : C) →
            CategoryTheory.Limits.IsColimit
              (CategoryTheory.Limits.CokernelCofork.ofπ (SSet.π₀.fromChainComplexXZero X R) ⋯)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.stdBasis_apply_isComplex_fst : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.mixedSpace K)
  (w : { w // w.IsComplex }), ((NumberField.mixedEmbedding.stdBasis K).repr x) (Sum.inr (w, 0)) = (x.2 w).re
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
CategoryTheory.OplaxFunctor.instInhabited : {B : Type u₁} → [inst : CategoryTheory.Bicategory B] → Inhabited (CategoryTheory.OplaxFunctor B B)
-- Aesop.Tree.Data
Aesop.instBEqGoalState.beq : Aesop.GoalState → Aesop.GoalState → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- Every split monomorphism is a regular monomorphism.  -/
CategoryTheory.RegularMono.ofIsSplitMono : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → (f : X ⟶ Y) → [CategoryTheory.IsSplitMono f] → CategoryTheory.RegularMono f
-- Lean.Data.Json.Basic
Lean.instDecidableEqJsonNumber.decEq : (x x_1 : Lean.JsonNumber) → Decidable (x = x_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom.mk.inj : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {inst : CategoryTheory.Category.{v₁, u₁} A}
  {inst_1 : CategoryTheory.Category.{v₂, u₂} B} {inst_2 : CategoryTheory.Category.{v₃, u₃} C}
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄}
  {inst_3 : CategoryTheory.Category.{v₄, u₄} X} {x y : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X}
  {fst : x.fst ⟶ y.fst} {snd : x.snd ⟶ y.snd}
  {w :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight fst F) y.iso.hom =
        CategoryTheory.CategoryStruct.comp x.iso.hom (CategoryTheory.Functor.whiskerRight snd G))
      CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom.w._autoParam}
  {fst_1 : x.fst ⟶ y.fst} {snd_1 : x.snd ⟶ y.snd}
  {w_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight fst_1 F) y.iso.hom =
        CategoryTheory.CategoryStruct.comp x.iso.hom (CategoryTheory.Functor.whiskerRight snd_1 G))
      CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom.w._autoParam},
  { fst := fst, snd := snd, w := w } = { fst := fst_1, snd := snd_1, w := w_1 } → fst = fst_1 ∧ snd = snd_1
-- Mathlib.Algebra.Ring.CompTypeclasses
/-- `σ'` is a left inverse of `σ'`  -/
RingHomInvPair.comp_eq₂ : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {inst : Semiring R₁} {inst_1 : Semiring R₂} {σ : R₁ →+* R₂}
  {σ' : outParam (R₂ →+* R₁)} [self : RingHomInvPair σ σ'], σ.comp σ' = RingHom.id R₂
-- Mathlib.Probability.Kernel.RadonNikodym
/-- Lebesgue decomposition of a finite kernel `κ` with respect to another one `η`.
`κ` is the sum of an absolutely continuous part `withDensity η (rnDeriv κ η)` and a singular part
`singularPart κ η`.  -/
ProbabilityTheory.Kernel.rnDeriv_add_singularPart : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ)
  [inst : ProbabilityTheory.IsFiniteKernel κ] [inst_1 : ProbabilityTheory.IsFiniteKernel η],
  η.withDensity (κ.rnDeriv η) + κ.singularPart η = κ
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.degreeLT_eq_span_X_pow : ∀ {R : Type u} [inst : Semiring R] [inst_1 : DecidableEq R] {n : ℕ},
  Polynomial.degreeLT R n = Submodule.span R ↑(Finset.image (fun n => Polynomial.X ^ n) (Finset.range n))
-- Mathlib.GroupTheory.Finiteness
AddMonoid.fg_of_monoid_fg : ∀ {M : Type u_1} [inst : Monoid M] [Monoid.FG M], AddMonoid.FG (Additive M)
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
/-- Natural transformations between functors lift to commutative group objects.  -/
CategoryTheory.Functor.mapCommGrpNatTrans : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.CartesianMonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                {F F' : CategoryTheory.Functor C D} →
                  [inst_6 : F.Braided] → [inst_7 : F'.Braided] → (F ⟶ F') → (F.mapCommGrp ⟶ F'.mapCommGrp)
-- Mathlib.Analysis.Normed.Operator.Conformal
isConformalMap_const_smul : ∀ {R : Type u_1} {M : Type u_2} [inst : NormedField R] [inst_1 : SeminormedAddCommGroup M] [inst_2 : NormedSpace R M]
  {c : R}, c ≠ 0 → IsConformalMap (c • ContinuousLinearMap.id R M)
-- Mathlib.Algebra.Category.Grp.Limits
/-- We show that the forgetful functor `CommGrpCat ⥤ GrpCat` creates limits.

All we need to do is notice that the limit point has a `CommGroup` instance available,
and then reuse the existing limit.
 -/
CommGrpCat.Forget₂.createsLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J CommGrpCat) → CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ CommGrpCat GrpCat)
-- Init.Data.Int.Order
Int.add_le_of_le_sub_right : ∀ {a b c : ℤ}, a ≤ c - b → a + b ≤ c
-- Std.Data.HashMap.Lemmas
Std.HashMap.toList_insert_perm : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {v : β}, (m.insert k v).toList.Perm ((k, v) :: List.filter (fun x_2 => decide ¬(k == x_2.1) = true) m.toList)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
derivWithin_csin : ∀ {f : ℂ → ℂ} {x : ℂ} {s : Set ℂ},
  DifferentiableWithinAt ℂ f s x →
    UniqueDiffWithinAt ℂ s x → derivWithin (fun x => Complex.sin (f x)) s x = Complex.cos (f x) * derivWithin f s x