mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.DefEqTransformations
/-- `unfold_projs at loc` unfolds projections of class instances at the given location.
This also exists as a `conv`-mode tactic.
 -/
Mathlib.Tactic.convUnfold_projs : Lean.ParserDescr
-- Mathlib.FieldTheory.Tower
/-- [Stacks Tag 09G5](https://stacks.math.columbia.edu/tag/09G5) -/
Module.Finite.right : ∀ (F : Type u) (K : Type v) (A : Type w) [inst : Semiring F] [inst_1 : Semiring K] [inst_2 : Module F K]
  [inst_3 : AddCommMonoid A] [inst_4 : Module K A] [inst_5 : Module F A] [IsScalarTower F K A] [hf : Module.Finite F A],
  Module.Finite K A
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ D` reflects limits, then `F.rightOp : C ⥤ Dᵒᵖ` reflects colimits.  -/
CategoryTheory.Limits.reflectsColimits_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.ReflectsLimits F],
  CategoryTheory.Limits.ReflectsColimits F.rightOp
-- Mathlib.Probability.Independence.Process.Basic
/-- Stochastic processes $((X^s_t)_{t \in T_s})_{s \in S}$ are mutually independent if
for all $s_1, ..., s_n$ and all $t^{s_i}_1, ..., t^{s_i}_{p_i}$ the families
$(X^{s_1}_{t^{s_1}_1}, ..., X^{s_1}_{t^{s_1}_{p_1}}), ...,
(X^{s_n}_{t^{s_n}_1}, ..., X^{s_n}_{t^{s_n}_{p_n}})$ are mutually independent.  -/
ProbabilityTheory.Kernel.iIndepFun.iIndepFun_process : ∀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {α : Type u_4} {mα : MeasurableSpace α}
  {κ : ProbabilityTheory.Kernel α Ω} {P : MeasureTheory.Measure α} {T : S → Type u_5} {𝓧 : (i : S) → T i → Type u_6}
  [inst : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)] {X : (i : S) → (j : T i) → Ω → 𝓧 i j},
  (∀ (i : S) (j : T i), Measurable (X i j)) →
    (∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)),
        ProbabilityTheory.Kernel.iIndepFun (fun i ω j => X (↑i) (↑j) ω) κ P) →
      ProbabilityTheory.Kernel.iIndepFun (fun i ω j => X i j ω) κ P
-- Init.Prelude
/-- A bitvector of the specified width.

This is represented as the underlying `Nat` number in both the runtime
and the kernel, inheriting all the special support for `Nat`.
 -/
BitVec : ℕ → Type
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.unzero_le_unzero : ∀ {α : Type u_1} [inst : LE α] {x y : WithZero α} (hx : x ≠ 0) (hy : y ≠ 0),
  WithZero.unzero hx ≤ WithZero.unzero hy ↔ x ≤ y
-- Mathlib.Algebra.Group.UniqueProds.Basic
_private.Mathlib.Algebra.Group.UniqueProds.Basic.0.UniqueProds.toIsLeftCancelMul : ∀ {G : Type u} [inst : Mul G] [UniqueProds G], IsLeftCancelMul G
-- Std.Sat.AIG.Basic
/-- The `Ref.cast` equivalent for `BinaryInput`.
 -/
Std.Sat.AIG.BinaryInput.cast : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig1 aig2 : Std.Sat.AIG α} → aig1.BinaryInput → aig1.decls.size ≤ aig2.decls.size → aig2.BinaryInput
-- Lean.Data.Lsp.Basic
Lean.Lsp.StaticRegistrationOptions : Type
-- Mathlib.Order.CompleteBooleanAlgebra
iSup_iInf_le : ∀ {α : Type u} {ι : Sort w} {κ : ι → Sort w'} [inst : CompleteLattice α] {f : (a : ι) → κ a → α},
  ⨆ a, ⨅ b, f a b ≤ ⨅ g, ⨆ a, f a (g a)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.iso_mapPullbackAdj_unit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y X : C} (f : Y ≅ X) (T : CategoryTheory.Over Y),
  (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj f.hom).unit.app T =
    CategoryTheory.Over.homMk (CategoryTheory.CategoryStruct.id T.left) ⋯
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.bolThen : Lean.Doc.Parser.BlockCtxt → Lean.Parser.ParserFn → String → Lean.Parser.ParserFn
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
continuous_cfcₙAux : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A] [inst_2 : StarRing A]
  [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A] [inst_6 : StarModule 𝕜 A]
  {p : A → Prop} {p₁ : Unitization 𝕜 A → Prop} (hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x) (a : A) (ha : p a)
  [inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁], Continuous ⇑(cfcₙAux ⋯ a ha)
-- Mathlib.Algebra.Group.WithOne.Basic
WithOne.mapMulHom_inj : ∀ {α : Type u} {β : Type v} [inst : Mul α] [inst_1 : Mul β] {f g : α →ₙ* β},
  WithOne.mapMulHom f = WithOne.mapMulHom g ↔ f = g
-- Mathlib.Algebra.Homology.Functor
/-- A complex of functors gives a functor to complexes.  -/
HomologicalComplex.asFunctor : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {V : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} V] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] →
          {ι : Type u_3} →
            {c : ComplexShape ι} →
              HomologicalComplex (CategoryTheory.Functor T V) c → CategoryTheory.Functor T (HomologicalComplex V c)
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.isLongestRevMatchAtChain_iff : ∀ {pat : String} {s : String.Slice} {pos₁ pos₂ : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAtChain pat pos₁ pos₂ ↔
    ∃ (h : pos₁ ≤ pos₂), ∃ n, (s.slice pos₁ pos₂ h).copy = String.join (List.replicate n pat)
-- Aesop.Tree.ExtractScript
Aesop.ExtractScript.lazyStepsToSteps : Aesop.DisplayRuleName → Option (Array Aesop.Script.LazyStep) → Lean.MetaM (Array Aesop.Script.Step)
-- Plausible.Gen
/-- Given two generators produces a tuple consisting out of the result of both  -/
Plausible.Gen.prodOf : {α : Type u} → {β : Type v} → Plausible.Gen α → Plausible.Gen β → Plausible.Gen (α × β)
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- A functor which preserves homology preserves cokernels.  -/
CategoryTheory.Functor.PreservesHomology.preservesCokernel : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] [F.PreservesHomology] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
/-- Coercion of an element of `K` into the completion.  -/
NumberField.InfinitePlace.Completion.instCoe : {K : Type u_1} → [inst : Field K] → (v : NumberField.InfinitePlace K) → Coe K v.Completion
-- Mathlib.Data.List.Perm.Basic
List.perm_replicate_append_replicate : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α} {a b : α} {m n : ℕ},
  a ≠ b → (l.Perm (List.replicate m a ++ List.replicate n b) ↔ List.count a l = m ∧ List.count b l = n ∧ l ⊆ [a, b])
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
SheafOfModules.Finite.hasFiniteLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  (R : CategoryTheory.Sheaf J RingCat), CategoryTheory.Limits.HasFiniteLimits (SheafOfModules R)
-- Mathlib.Order.ModularLattice
Codisjoint.isCompl_inf_left_of_isCompl_inf_right : ∀ {α : Type u_1} {a b c : α} [inst : Lattice α] [inst_1 : BoundedOrder α] [IsModularLattice α],
  Codisjoint b c → IsCompl a (b ⊓ c) → IsCompl (a ⊓ b) c
-- Init.Data.UInt.Bitwise
instCommutativeUInt32HAnd : Std.Commutative fun x1 x2 => x1 &&& x2
-- Std.Time.DateTime.Timestamp
/-- Adds a `Nanosecond.Offset` to the given `Timestamp`.
 -/
Std.Time.Timestamp.addNanoseconds : Std.Time.Timestamp → Std.Time.Nanosecond.Offset → Std.Time.Timestamp
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.map.eq_1 : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (φ : W.LeftFraction X Y) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L),
  φ.map L hL = CategoryTheory.CategoryStruct.comp (L.map φ.f) (CategoryTheory.inv (L.map φ.s))
-- Init.Grind.Order
Lean.Grind.Order.lt_eq_true_of_lt_k : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [inst_3 : Std.IsPreorder α]
  [inst_4 : Lean.Grind.Ring α] [Lean.Grind.OrderedRing α] {a b : α} {k₁ k₂ : ℤ},
  k₁.ble' k₂ = true → a < b + ↑k₁ → (a < b + ↑k₂) = True
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.isEmpty_inter_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m₂.isEmpty = true → (m₁ ∩ m₂).isEmpty = true
-- Lean.Meta.Sym.Offset
Lean.Meta.Sym.instInhabitedOffset : Inhabited Lean.Meta.Sym.Offset
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_congr : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] [inst_2 : Inhabited α] {l : List ((a : α) × β a)}
  {k k' : α}, (k == k') = true → Std.Internal.List.getKey! k l = Std.Internal.List.getKey! k' l
-- Mathlib.RingTheory.Etale.Basic
Algebra.Etale.formallyEtale : ∀ {R : Type u} {A : Type v} {inst : CommRing R} {inst_1 : CommRing A} {inst_2 : Algebra R A} [self : Algebra.Etale R A],
  Algebra.FormallyEtale R A
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
/-- `linearIndepOn_pair_iff` is a simpler version over fields.  -/
LinearIndepOn.pair_iff : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {i j : ι}
  (f : ι → M), i ≠ j → (LinearIndepOn R f {i, j} ↔ ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Finpartition.nonUniforms_bot : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : DecidableEq α] {A : Finset α} (G : SimpleGraph α) [inst_4 : DecidableRel G.Adj] {ε : 𝕜},
  0 < ε → ⊥.nonUniforms G ε = ∅
-- Lean.Data.Options
Lean.OptionDeprecation.text? : Lean.OptionDeprecation → Option String
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.ofSubsingleton.congr_simp : ∀ (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] [inst_7 : Subsingleton ι] (i i_1 : ι),
  i = i_1 → ContinuousAlternatingMap.ofSubsingleton R M N i = ContinuousAlternatingMap.ofSubsingleton R M N i_1
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.ExprCnstr.toNormPoly : Nat.Internal.Linear.ExprCnstr → Nat.Internal.Linear.PolyCnstr
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.Lp.const_val : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α)
  [inst : NormedAddCommGroup E] [inst_1 : MeasureTheory.IsFiniteMeasure μ] (c : E),
  ↑((MeasureTheory.Lp.const p μ) c) = MeasureTheory.AEEqFun.const α c
-- Init.Data.List.Nat.Basic
List.dropLast_reverse : ∀ {α : Type u_1} {l : List α}, l.reverse.dropLast = l.tail.reverse
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.ofRingHom_symm : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S) (g : S →+* R)
  (h₁ : f.comp g = RingHom.id S) (h₂ : g.comp f = RingHom.id R),
  (RingEquiv.ofRingHom f g h₁ h₂).symm = RingEquiv.ofRingHom g f h₂ h₁
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueProds.mk : ∀ {G : Type u_1} [inst : Mul G],
  (∀ {A B : Finset G}, A.Nonempty → B.Nonempty → ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0) → UniqueProds G
-- Mathlib.Data.ENNReal.Operations
/-- See `ENNReal.sub_eq_of_eq_add'` for a version assuming that `a = c + b` itself is finite rather
than `b`.  -/
ENNReal.sub_eq_of_eq_add : ∀ {a b c : ENNReal}, b ≠ ⊤ → a = c + b → a - b = c
-- Mathlib.RingTheory.Kaehler.Polynomial
/-- The relative differential module of a polynomial algebra `R[σ]` is the free module generated by
`{ dx | x ∈ σ }`. Also see `KaehlerDifferential.mvPolynomialBasis`.  -/
KaehlerDifferential.mvPolynomialEquiv : (R : Type u) → [inst : CommRing R] → (σ : Type u_1) → Ω[MvPolynomial σ R⁄R] ≃ₗ[MvPolynomial σ R] σ →₀ MvPolynomial σ R
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn'_rcc : ∀ {α β : Type u} {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  [inst_2 : LE α] [inst_3 : DecidableLE α] [inst_4 : Std.PRange.UpwardEnumerable α] [inst_5 : Std.Rxc.IsAlwaysFinite α]
  [inst_6 : Std.PRange.LawfulUpwardEnumerable α] [inst_7 : Std.PRange.LawfulUpwardEnumerableLE α] {xs : Std.Rcc α}
  {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Std.Do.Invariant xs.toList β ps),
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f cur ⋯ b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
          | ForInStep.done b' => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'),
          inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := xs.toList, property := ⋯ }, init)⦄
      forIn' xs init f ⦃(fun b => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b), inv.2)⦄
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonPlainTermGoal.fromJson : Lean.Json → Except String Lean.Lsp.PlainTermGoal
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- **Ruzsa's triangle inequality**. Subtraction version.  -/
Finset.ruzsa_triangle_inequality_sub_sub_sub : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddGroup G] (A B C : Finset G),
  (A - C).card * B.card ≤ (A - B).card * (C - B).card
-- Mathlib.Logic.Nontrivial.Basic
nontrivial_prod_right : ∀ {α : Type u_1} {β : Type u_2} [Nonempty α] [Nontrivial β], Nontrivial (α × β)
-- Lean.Elab.DocString
Lean.Doc.State.mk.injEq : ∀ (scopes : List Lean.Elab.Command.Scope) (openDecls : List Lean.OpenDecl) (lctx : Lean.LocalContext)
  (localInstances : Lean.LocalInstances) (options : Lean.Options) (scopes_1 : List Lean.Elab.Command.Scope)
  (openDecls_1 : List Lean.OpenDecl) (lctx_1 : Lean.LocalContext) (localInstances_1 : Lean.LocalInstances)
  (options_1 : Lean.Options),
  ({ scopes := scopes, openDecls := openDecls, lctx := lctx, localInstances := localInstances, options := options } =
      { scopes := scopes_1, openDecls := openDecls_1, lctx := lctx_1, localInstances := localInstances_1,
        options := options_1 }) =
    (scopes = scopes_1 ∧
      openDecls = openDecls_1 ∧ lctx = lctx_1 ∧ localInstances = localInstances_1 ∧ options = options_1)
-- Init.Data.BitVec.Lemmas
BitVec.toFin_sub : ∀ {n : ℕ} (x y : BitVec n), (x - y).toFin = x.toFin - y.toFin
-- Mathlib.Order.Concept
Concept.swapEquiv_symm_apply : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (a : Concept β α (Function.swap r)),
  (RelIso.symm Concept.swapEquiv) a = (⇑OrderDual.toDual ∘ Concept.swap) a
-- Mathlib.Order.Filter.Ker
Filter.ker_inf : ∀ {α : Type u_2} (f g : Filter α), (f ⊓ g).ker = f.ker ∩ g.ker
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.shiftIso_hom_app_comp : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : F.ShiftSequence M] (n m mn : M) (hnm : m + n = mn) (a a' a'' : M)
  (ha' : n + a = a') (ha'' : m + a' = a'') (X : C),
  CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').hom.app ((CategoryTheory.shiftFunctor C m).obj X))
      ((F.shiftIso m a' a'' ha'').hom.app X) =
    CategoryTheory.CategoryStruct.comp ((F.shift a).map ((CategoryTheory.shiftFunctorAdd' C m n mn hnm).inv.app X))
      ((F.shiftIso mn a a'' ⋯).hom.app X)
-- Mathlib.RingTheory.Extension.Presentation.Core
/-- The core of a presentation is the subalgebra generated by the coefficients of the relations.  -/
Algebra.Presentation.core : {R : Type u_1} →
  {S : Type u_2} →
    {ι : Type u_3} →
      {σ : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Algebra.Presentation R S ι σ → Subalgebra ℤ R
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
IsCyclic.index_powMonoidHom_range : ∀ (G : Type u_2) [inst : CommGroup G] [IsCyclic G] [Finite G] (d : ℕ), (powMonoidHom d).range.index = (Nat.card G).gcd d
-- Mathlib.Order.Atoms
/-- Representation theorem for complete atomic boolean algebras:
For a complete atomic Boolean algebra `α`, `toSetOfIsAtom` is an order isomorphism
between `α` and the set of subsets of its atoms.
 -/
CompleteAtomicBooleanAlgebra.toSetOfIsAtom : {α : Type u_4} → [inst : CompleteAtomicBooleanAlgebra α] → α ≃o Set { a // IsAtom a }
-- Lean.Elab.Command
Lean.Elab.Command.instMonadRecDepthCommandElabM : Lean.MonadRecDepth Lean.Elab.Command.CommandElabM
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.State.goals : Lean.Elab.Tactic.State → List Lean.MVarId
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.comp_fderivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {s : Set G} {x : G},
  UniqueDiffWithinAt 𝕜 s x → fderivWithin 𝕜 (⇑iso ∘ f) s x = ↑iso ∘SL fderivWithin 𝕜 f s x
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivAt.differentiableAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜}, HasDerivAt f f' x → DifferentiableAt 𝕜 f x
-- Init.Prelude
/-- Make name `s₁.s₂`  -/
Lean.Name.mkStr2 : String → String → Lean.Name
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {km : α}, t.minKey? = some km → t.getKey! km = km
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_zero : ∀ {α : Type u} [inst : Semiring α], Ideal.span 0 = ⊥
-- Mathlib.Algebra.Homology.ShortComplex.Limits
/-- `limitCone F` becomes limit after the application of `π₃ : ShortComplex C ⥤ C`.  -/
CategoryTheory.ShortComplex.isLimitπ₃MapConeLimitCone : {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] →
          (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) →
            [inst_3 : CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₁)] →
              [inst_4 : CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₂)] →
                [inst_5 : CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₃)] →
                  CategoryTheory.Limits.IsLimit
                    (CategoryTheory.ShortComplex.π₃.mapCone (CategoryTheory.ShortComplex.limitCone F))
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_insertList_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys toInsert →
      Std.Internal.List.containsKey k l = false →
        Std.Internal.List.getValueCast? k (Std.Internal.List.insertList l toInsert) =
          Std.Internal.List.getValueCast? k toInsert
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.pow_mem : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  {x : L}, x ∈ S → ∀ (n : ℤ), x ^ n ∈ S
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.pi_condition_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I)
  {c : CategoryTheory.Limits.Fan I.left} (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right}
  (hd : CategoryTheory.Limits.IsLimit d) {Z : C} (h : d.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc K.ι)
      (CategoryTheory.CategoryStruct.comp (I.fstPiMapOfIsLimit c hd) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc K.ι)
      (CategoryTheory.CategoryStruct.comp (I.sndPiMapOfIsLimit c hd) h)
-- Mathlib.Topology.List
List.tendsto_insertIdx : ∀ {α : Type u_1} [inst : TopologicalSpace α] {β : Type u_3} {n : ℕ} {a : α} {l : List α} {f : β → α} {g : β → List α}
  {b : Filter β},
  Filter.Tendsto f b (nhds a) →
    Filter.Tendsto g b (nhds l) → Filter.Tendsto (fun b => (g b).insertIdx n (f b)) b (nhds (l.insertIdx n a))
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
iteratedFDerivWithin_zero_apply : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} (m : Fin 0 → E), (iteratedFDerivWithin 𝕜 0 f s x) m = f x
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instNatCast : {α : Type u_1} →
  {β : Type u_2} → [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → [NatCast β] → NatCast C(α, β)
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.index_union_eq : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G]
  (K₁ K₂ : TopologicalSpace.Compacts G) {V : Set G},
  (interior V).Nonempty →
    Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹) →
      MeasureTheory.Measure.haar.index (K₁.carrier ∪ K₂.carrier) V =
        MeasureTheory.Measure.haar.index K₁.carrier V + MeasureTheory.Measure.haar.index K₂.carrier V
-- Mathlib.RingTheory.Derivation.MapCoeffs
/-- A specialization of `Derivation.mapCoeffs` for the case of a differential ring.
 -/
Differential.mapCoeffs : {A : Type u_1} → [inst : CommRing A] → [Differential A] → Derivation ℤ (Polynomial A) (Polynomial A)
-- Mathlib.Order.Hom.Bounded
map_eq_bot_iff : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : LE α] [inst_2 : OrderBot α]
  [inst_3 : PartialOrder β] [inst_4 : OrderBot β] [OrderIsoClass F α β] (f : F) {a : α}, f a = ⊥ ↔ a = ⊥
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.coe_forget₂_obj : ∀ (X : AddCommMonCat), ↑((CategoryTheory.forget₂ AddCommMonCat AddMonCat).obj X) = ↑X
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- A family `𝓕 : ι → β → α` is uniformly equicontinuous iff `range 𝓕` is uniformly equicontinuous,
i.e the family `(↑) : range F → β → α` is uniformly equicontinuous.  -/
uniformEquicontinuous_iff_range : ∀ {ι : Type u_1} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] {F : ι → β → α},
  UniformEquicontinuous F ↔ UniformEquicontinuous Subtype.val
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.not_isUnit : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, FiniteMultiplicity a b → ¬IsUnit a
-- Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
/-- The isomorphism expressing the commutation of the functor `opOp C : C ⥤ Cᵒᵖᵒᵖ`
with the shift by `n : ℤ`.  -/
CategoryTheory.Pretriangulated.Opposite.OpOpCommShift.iso : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      (n : ℤ) →
        (CategoryTheory.shiftFunctor C n).comp (CategoryTheory.opOp C) ≅
          (CategoryTheory.opOp C).comp (CategoryTheory.shiftFunctor Cᵒᵖᵒᵖ n)
-- Mathlib.Probability.Martingale.OptionalStopping
/-- The stopped process of a submartingale with respect to a stopping time is a submartingale.  -/
MeasureTheory.Submartingale.stoppedProcess : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0}
  {f : ℕ → Ω → ℝ} {τ : Ω → ℕ∞} [MeasureTheory.SigmaFiniteFiltration μ 𝒢],
  MeasureTheory.Submartingale f 𝒢 μ →
    MeasureTheory.IsStoppingTime 𝒢 τ → MeasureTheory.Submartingale (MeasureTheory.stoppedProcess f τ) 𝒢 μ