mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Order.OrderClosedExtr
/-- If `f` is monotone on `Ioc a b` and antitone on `Ico b c` then `f` has
a local maximum at `b`.  -/
isLocalMax_of_mono_anti : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {β : Type u_2}
  [inst_3 : Preorder β] {a b c : α},
  a < b → b < c → ∀ {f : α → β}, MonotoneOn f (Set.Ioc a b) → AntitoneOn f (Set.Ico b c) → IsLocalMax f b
-- Std.Data.DTreeMap.Internal.Def
Std.DTreeMap.Internal.Impl.toListModel_leaf : ∀ {α : Type u} {β : α → Type v}, Std.DTreeMap.Internal.Impl.leaf.toListModel = []
-- Mathlib.Data.ENNReal.Holder
/-- assumes `q ≠ 0` instead of `r ≠ 0`.  -/
ENNReal.HolderTriple.inv_sub_inv_eq_inv' : ∀ (p q r : ENNReal) [p.HolderTriple q r], q ≠ 0 → r⁻¹ - q⁻¹ = p⁻¹
-- Lean.Elab.Tactic.Ext
/-- Postprocessor for `withExt` which runs `rintro` with the given patterns when the target is a
pi type.
 -/
_private.Lean.Elab.Tactic.Ext.0.Lean.Elab.Tactic.Ext.tryIntros : {m : Type → Type u_1} →
  [Monad m] →
    [MonadLiftT Lean.Elab.TermElabM m] →
      Lean.MVarId → List (Lean.TSyntax `rcasesPat) → (Lean.MVarId → List (Lean.TSyntax `rcasesPat) → m ℕ) → m ℕ
-- Mathlib.Order.RelIso.Basic
RelEmbedding.sumLiftRelMap_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop}
  {u : δ → δ → Prop} (f : r ↪r s) (g : t ↪r u) (a : α ⊕ γ), (f.sumLiftRelMap g) a = Sum.map (⇑f) (⇑g) a
-- Mathlib.Tactic.FBinop
FBinopElab.SRec.name : FBinopElab.SRec → Lean.Name
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.toRingEquiv_toRingHom : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (e : A ≃ₐc[R] B), ↑e.toAlgEquiv.toRingEquiv = ↑e
-- Mathlib.Order.Preorder.Chain
IsChain.preimage_iso_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] {t : Set β} {φ : α ≃o β},
  IsChain (fun x1 x2 => x1 ≤ x2) (⇑φ ⁻¹' t) ↔ IsChain (fun x1 x2 => x1 ≤ x2) t
-- Mathlib.Topology.Algebra.Monoid
Inseparable.nsmul : ∀ {M : Type u_6} [inst : AddMonoid M] [inst_1 : TopologicalSpace M] [ContinuousAdd M] {a b : M},
  Inseparable a b → ∀ (n : ℕ), Inseparable (n • a) (n • b)
-- Mathlib.NumberTheory.Modular
ModularGroup.eq_zero_of_mem_fdo_of_T_zpow_mem_fdo : ∀ {z : UpperHalfPlane} {n : ℤ}, z ∈ ModularGroup.fdo → ModularGroup.T ^ n • z ∈ ModularGroup.fdo → n = 0
-- Init.Meta.Defs
/-- Creates a group node, as if it were parsed by `Lean.Parser.group`.
 -/
Lean.mkGroupNode : optParam (Array Lean.Syntax) #[] → Lean.Syntax
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.getEscapedNameParts? : List String → Lean.Name → Option (List String)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Iic_mul_Iic_subset' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α] [MulLeftMono α] [MulRightMono α] (a b : α),
  Set.Iic a * Set.Iic b ⊆ Set.Iic (a * b)
-- Mathlib.Order.CompleteLattice.Defs
ofDual_iSup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : InfSet α] (f : ι → αᵒᵈ),
  OrderDual.ofDual (⨆ i, f i) = ⨅ i, OrderDual.ofDual (f i)
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.ExceptT.bindCont.match_1.eq_2 : ∀ {ε α : Type u_1} (motive : Except ε α → Sort u_2) (e : ε) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.error e with
    | Except.ok a => h_1 a
    | Except.error e => h_2 e) =
    h_2 e
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.Hom.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} {app : (X : Cᵒᵖ) → M₁.obj X ⟶ M₂.obj X}
  {naturality :
    autoParam
      (∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
        CategoryTheory.CategoryStruct.comp (M₁.map f)
            ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (app Y)) =
          CategoryTheory.CategoryStruct.comp (app X) (M₂.map f))
      PresheafOfModules.Hom.naturality._autoParam}
  {app_1 : (X : Cᵒᵖ) → M₁.obj X ⟶ M₂.obj X}
  {naturality_1 :
    autoParam
      (∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
        CategoryTheory.CategoryStruct.comp (M₁.map f)
            ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (app_1 Y)) =
          CategoryTheory.CategoryStruct.comp (app_1 X) (M₂.map f))
      PresheafOfModules.Hom.naturality._autoParam},
  { app := app, naturality := naturality } = { app := app_1, naturality := naturality_1 } → app = app_1
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.pi_empty : ∀ {ι : Type u_4} {M : ι → Type u_5} [inst : (i : ι) → AddZeroClass (M i)] (H : (i : ι) → AddSubmonoid (M i)),
  AddSubmonoid.pi ∅ H = ⊤
-- Init.Data.SInt.Lemmas
Int64.ofIntClamp_int8ToInt : ∀ (x : Int8), Int64.ofIntClamp x.toInt = x.toInt64
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isLittleO_norm_pow_norm_pow : ∀ {E' : Type u_6} [inst : SeminormedAddCommGroup E'] {m n : ℕ}, m < n → (fun x => ‖x‖ ^ n) =o[nhds 0] fun x => ‖x‖ ^ m
-- Std.Net.Addr
Std.Net.SocketAddressV6.port : Std.Net.SocketAddressV6 → UInt16
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.ball_eq_ball' : ∀ {α : Type u} [inst : PseudoMetricSpace α] (ε : ℝ) (x : α),
  UniformSpace.ball x {p | dist p.1 p.2 < ε} = Metric.ball x ε
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
/-- Given `φ : F ⟶ G`, this is the cocycle in `Cocycle K (mappingCone φ) n` that is
constructed from `α : Cochain K F m` (with `n + 1 = m`) and `β : Cocycle K G n`,
when a suitable cocycle relation is satisfied.  -/
CochainComplex.mappingCone.liftCocycle : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {F G : CochainComplex C ℤ} →
        (φ : F ⟶ G) →
          [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
            {K : CochainComplex C ℤ} →
              {n m : ℤ} →
                (α : CochainComplex.HomComplex.Cocycle K F m) →
                  (β : CochainComplex.HomComplex.Cochain K G n) →
                    n + 1 = m →
                      CochainComplex.HomComplex.δ n m β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0 →
                        CochainComplex.HomComplex.Cocycle K (CochainComplex.mappingCone φ) n
-- Mathlib.RingTheory.Kaehler.Polynomial
KaehlerDifferential.polynomial_D_apply : ∀ (R : Type u) [inst : CommRing R] (P : Polynomial R),
  (KaehlerDifferential.D R (Polynomial R)) P =
    Polynomial.derivative P • (KaehlerDifferential.D R (Polynomial R)) Polynomial.X
-- Init.Data.String.Basic
String.Slice.Pos.ofSliceTo_endPos : ∀ {s : String.Slice} {pos : s.Pos}, String.Slice.Pos.ofSliceTo (s.sliceTo pos).endPos = pos
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtDTreeMap α β cmp)
  (e_t : t = t_1) (a a_1 : α) (e_a : a = a_1) (h : a ∈ t), t.getKey a h = t_1.getKey a_1 ⋯
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
/-- An `n`-preprimitive action is `n`-pretransitive.  -/
MulAction.IsMultiplyPreprimitive.isMultiplyPretransitive : ∀ (M : Type u_1) (α : Type u_2) {inst : Group M} {inst_1 : MulAction M α} (n : ℕ)
  [self : MulAction.IsMultiplyPreprimitive M α n], MulAction.IsMultiplyPretransitive M α n
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.le_shiftClosure : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {A : Type u_2}
  [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A], P ≤ P.shiftClosure A
-- Mathlib.Order.BoundedOrder.Basic
eq_top_of_bot_eq_top : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : BoundedOrder α], ⊥ = ⊤ → ∀ (x : α), x = ⊤
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
setIntegral_withDensity_eq_setIntegral_toReal_smul₀' : ∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [MeasureTheory.SFinite μ] {f : X → ENNReal} (s : Set X),
  AEMeasurable f (μ.restrict s) →
    (∀ᵐ (x : X) ∂μ.restrict s, f x < ⊤) →
      ∀ (g : X → E), ∫ (x : X) in s, g x ∂μ.withDensity f = ∫ (x : X) in s, (f x).toReal • g x ∂μ
-- Lean.ParserCompiler
Lean.ParserCompiler.Context.tyName : {α : Type} → Lean.ParserCompiler.Context α → Lean.Name
-- Mathlib.Computability.NFA
_private.Mathlib.Computability.NFA.0.NFA.mem_acceptsFrom_sep_fact : ∀ {α : Type u} {σ : Type v} (M : NFA α σ) {S : Set σ} {p : Prop} {x : List α},
  x ∈ M.acceptsFrom {s | s ∈ S ∧ p} ↔ x ∈ M.acceptsFrom S ∧ p
-- Mathlib.LinearAlgebra.TensorProduct.Basic
/-- Given a semilinear map `M ⊗ N → P`, compose it with the canonical bilinear map
`M → N → M ⊗ N` to form a bilinear map `M → N → P`.  -/
TensorProduct.curry : {R : Type u_1} →
  {R₂ : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring R₂] →
        {σ₁₂ : R →+* R₂} →
          {M : Type u_7} →
            {N : Type u_8} →
              {P₂ : Type u_17} →
                [inst_2 : AddCommMonoid M] →
                  [inst_3 : AddCommMonoid N] →
                    [inst_4 : AddCommMonoid P₂] →
                      [inst_5 : Module R M] →
                        [inst_6 : Module R N] →
                          [inst_7 : Module R₂ P₂] → (TensorProduct R M N →ₛₗ[σ₁₂] P₂) → M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂
-- Init.Data.Nat.Internal.SOM
_private.Init.Data.Nat.Internal.SOM.0.Nat.Internal.SOM.Poly.mul.go : Nat.Internal.SOM.Poly → Nat.Internal.SOM.Poly → Nat.Internal.SOM.Poly → Nat.Internal.SOM.Poly
-- Mathlib.Topology.Algebra.Module.Equiv
/-- Continuous linear equivalences between modules. We only put the type classes that are necessary
for the definition, although in applications `M` and `M₂` will be topological modules over the
topological semiring `R`.  -/
«term_≃L[_]_» : Lean.TrailingParserDescr
-- Mathlib.Data.Sum.Interval
Finset.sumLexLift_inr_inr : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6}
  (f₁ : α₁ → β₁ → Finset γ₁) (f₂ : α₂ → β₂ → Finset γ₂) (g₁ : α₁ → β₂ → Finset γ₁) (g₂ : α₁ → β₂ → Finset γ₂) (a : α₂)
  (b : β₂), Finset.sumLexLift f₁ f₂ g₁ g₂ (Sum.inr a) (Sum.inr b) = Finset.map { toFun := Sum.inr, inj' := ⋯ } (f₂ a b)
-- Lean.Meta.Tactic.Split
_private.Lean.Meta.Tactic.Split.0.Lean.Meta.Split.simpMatch.pre : Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step
-- Lean.Declaration
Lean.Declaration.quotDecl : Lean.Declaration
-- Mathlib.CategoryTheory.Distributive.Monoidal
/-- The forward direction of the right distributivity isomorphism is equal to the cogap morphism
`coprod.desc (coprod.inl ▷ _) (coprod.inr ▷ _) : (Y ⊗ X) ⨿ (Z ⊗ X) ⟶ (Y ⨿ Z) ⊗ X`.  -/
CategoryTheory.rightDistrib_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_3 : CategoryTheory.IsMonoidalRightDistrib C] {X Y Z : C},
  (∂R X Y Z).hom =
    CategoryTheory.Limits.coprod.desc
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.coprod.inl X)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.coprod.inr X)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.IsBase.eq_of_superset_spanning : ∀ {α : Type u_2} {M : Matroid α} {X B : Set α}, M.IsBase B → M.Spanning X → X ⊆ B → B = X
-- Mathlib.Algebra.Group.Prod
addAddMonoidHom.eq_1 : ∀ {α : Type u_6} [inst : AddCommMonoid α], addAddMonoidHom = { toFun := addAddHom.toFun, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Logic.Function.Basic
Pi.map_comp_map : ∀ {ι : Type u_3} {α : ι → Type u_4} {β : ι → Type u_5} {γ : ι → Type u_6} (f : (i : ι) → α i → β i)
  (g : (i : ι) → β i → γ i), Pi.map g ∘ Pi.map f = Pi.map fun i => g i ∘ f i
-- Mathlib.Algebra.Group.Center
/-- The center of an additive magma.  -/
Set.addCenter : (M : Type u_1) → [Add M] → Set M
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.root_X_sub_C : ∀ {R : Type u} {a b : R} [inst : Ring R], (Polynomial.X - Polynomial.C a).IsRoot b ↔ a = b
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.minKey!_modify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α} {f : β → β},
      (Std.DTreeMap.Raw.Const.modify t k f).isEmpty = false →
        (Std.DTreeMap.Raw.Const.modify t k f).minKey! = if cmp t.minKey! k = Ordering.eq then k else t.minKey!
-- Mathlib.RingTheory.Kaehler.TensorProduct
KaehlerDifferential.tensorKaehlerEquiv.congr_simp : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  [h : Algebra.IsPushout R S A B],
  KaehlerDifferential.tensorKaehlerEquiv R S A B = KaehlerDifferential.tensorKaehlerEquiv R S A B
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unmop_tensorObj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : Cᴹᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).unmop =
    CategoryTheory.MonoidalCategoryStruct.tensorObj Y.unmop X.unmop
-- Init.Data.Array.Lemmas
Array.getElem_range' : ∀ {start size step i : ℕ} (h : i < (Array.range' start size step).size),
  (Array.range' start size step)[i] = start + step * i
-- Mathlib.Topology.Algebra.InfiniteSum.Order
hasSum_le : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : AddCommMonoid α] [inst_1 : Preorder α]
  [IsOrderedAddMonoid α] [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {f g : ι → α} {a₁ a₂ : α},
  (∀ (i : ι), f i ≤ g i) → HasSum f a₁ L → HasSum g a₂ L → ∀ [L.NeBot], a₁ ≤ a₂
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun_iff_measure_inter_preimage_eq_mul : ∀ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_10} {β : ι → Type u_11}
  {m : (x : ι) → MeasurableSpace (β x)} {f : (i : ι) → Ω → β i},
  ProbabilityTheory.iIndepFun f μ ↔
    ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
      (∀ i ∈ S, MeasurableSet (sets i)) → μ (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, μ (f i ⁻¹' sets i)
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `Meromorphic.inv` -/
Meromorphic.fun_inv : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f : 𝕜 → 𝕜'}, Meromorphic f → Meromorphic fun i => (f i)⁻¹
-- Mathlib.GroupTheory.OrderOfElement
RightCancelMonoid.pow_inj_iff_of_orderOf_eq_zero : ∀ {G : Type u_1} [inst : RightCancelMonoid G] {x : G}, orderOf x = 0 → ∀ {n m : ℕ}, x ^ n = x ^ m ↔ n = m
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
NonUnitalContinuousFunctionalCalculus.mk : ∀ {R : Type u_1} {A : Type u_2} {p : outParam (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],
  p 0 →
    ∀ [compactSpace_quasispectrum : ∀ (a : A), CompactSpace ↑(quasispectrum R a)],
      (∀ (a : A),
          p a →
            ∃ φ,
              Continuous ⇑φ ∧
                Function.Injective ⇑φ ∧
                  φ
                        { toContinuousMap := ContinuousMap.restrict (quasispectrum R a) (ContinuousMap.id R),
                          map_zero' := ⋯ } =
                      a ∧
                    (∀ (f : ContinuousMapZero (↑(quasispectrum R a)) R), quasispectrum R (φ f) = Set.range ⇑f) ∧
                      ∀ (f : ContinuousMapZero (↑(quasispectrum R a)) R), p (φ f)) →
        NonUnitalContinuousFunctionalCalculus R A p
-- Mathlib.Algebra.Order.Ring.Abs
pow_eq_neg_pow_iff : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a b : R} {n : ℕ},
  b ≠ 0 → (a ^ n = -b ^ n ↔ a = -b ∧ Odd n)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.isUniquelyCodimOneFace : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) [h.IsProper] (s : h.ι),
  (h.type₂ s).IsUniquelyCodimOneFace (h.type₁ s).toS
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
LinearIsometryEquiv.comp_hasFDerivAt_iff' : ∀ {𝕜 : 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 ≃ₗᵢ[𝕜] F) {f : G → E} {x : G} {f' : G →L[𝕜] F},
  HasFDerivAt (⇑iso ∘ f) f' x ↔ HasFDerivAt f (↑↑iso.symm ∘SL f') x
-- Lean.Meta.Basic
/-- When `Context.trackZetaDelta == true`, then any let-decl free variable that is zetaDelta-expanded by `MetaM` is stored in `zetaDeltaFVarIds`.  -/
Lean.Meta.State.zetaDeltaFVarIds : Lean.Meta.State → Lean.FVarIdSet
-- Mathlib.ModelTheory.Order
FirstOrder.Language.orderLHom_order : FirstOrder.Language.order.orderLHom = FirstOrder.Language.LHom.id FirstOrder.Language.order
-- Mathlib.AlgebraicTopology.SimplicialObject.II
SimplexCategory.II.finset.eq_1 : ∀ {n m : ℕ} (f : Fin (n + 1) →o Fin (m + 1)) (x : Fin (m + 2)),
  SimplexCategory.II.finset f x =
    {i | i = Fin.last (n + 1) ∨ ∃ (h : i ≠ Fin.last (n + 1)), x ≤ (f (i.castPred h)).castSucc}
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.mapₐ_injective_of_injective : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_5} [inst_1 : CommSemiring A] [inst_2 : Algebra R A] {B : Type u_6}
  [inst_3 : CommSemiring B] [inst_4 : Algebra R B] {Aₚ : Type u_7} [inst_5 : CommSemiring Aₚ] [inst_6 : Algebra A Aₚ]
  [inst_7 : Algebra R Aₚ] [inst_8 : IsScalarTower R A Aₚ] {Bₚ : Type u_8} [inst_9 : CommSemiring Bₚ]
  [inst_10 : Algebra B Bₚ] [inst_11 : Algebra R Bₚ] [inst_12 : IsScalarTower R B Bₚ] {f : A →ₐ[R] B} (a : A)
  [inst_13 : IsLocalization.Away a Aₚ] [inst_14 : IsLocalization.Away (f a) Bₚ],
  Function.Injective ⇑f → Function.Injective ⇑(IsLocalization.Away.mapₐ Aₚ Bₚ f a)
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.inf_sup_assoc_of_le_of_submodule_le : ∀ {E : Type u_2} {R : Type u_5} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup E] [inst_4 : Module R E] {C : PointedCone R E} (D : PointedCone R E) {S : Submodule R E},
  ↑S ≤ C → C ⊓ D ⊔ ↑S = C ⊓ (D ⊔ ↑S)
-- Mathlib.LinearAlgebra.Matrix.Stochastic
/-- Left left-multiplication by column stochastic preserves `ℓ₁ norm`  -/
Matrix.mulVec_dotProduct_one_eq_one_colStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {M : Matrix n n R} {x : n → R},
  M ∈ Matrix.colStochastic R n → 1 ⬝ᵥ x = 1 → 1 ⬝ᵥ M.mulVec x = 1
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.toSpanSingletonCLE_apply_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : IsTopologicalAddGroup E] [inst_5 : ContinuousSMul 𝕜 E] (x : E) (b : 𝕜),
  (ContinuousLinearMap.toSpanSingletonCLE x) b = b • x
-- Std.Do.Triple.SpecLemmas
/-- The elements before to the current position in the list.
 -/
List.Cursor.prefix : {α : Type u} → {l : List α} → l.Cursor → List α
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.fg_of_isUnit : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (I : FractionalIdeal S P), IsUnit I → (↑I).FG
-- Mathlib.Algebra.Vertex.VertexOperator
VertexOperator.ncoeff_of_coeff : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  (f : ℤ → Module.End R V) (hf : ∀ (x : V), BddBelow (Function.support fun y => (f y) x)) (n : ℤ),
  VertexOperator.ncoeff (VertexOperator.of_coeff f hf) n = f (-n - 1)
-- Mathlib.Data.Finset.Image
/-- Reverse of `Finset.image_image`. The `Finset` analogue of `Set.image_comp`.  -/
Finset.image_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : DecidableEq β] {f : α → β} {s : Finset α}
  [inst_1 : DecidableEq γ] {g : β → γ}, Finset.image (g ∘ f) s = Finset.image g (Finset.image f s)
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.ext : ∀ {𝒮 : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} 𝒮}
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {x y : F.CoGrothendieck},
  x.base = y.base → x.fiber ≍ y.fiber → x = y
-- Init.Data.List.ToArrayImpl
/-- Auxiliary definition for `List.toArray`.
`List.toArrayAux as r = r ++ as.toArray`
 -/
List.toArrayAux : {α : Type u_1} → List α → Array α → Array α
-- Mathlib.Algebra.Order.GroupWithZero.Lex
/-- Given linearly ordered groups with zero M, N, the natural inclusion ordered homomorphism from
M to `WithZero (Mˣ ×ₗ Nˣ)`, which is the linearly ordered group with zero that can be identified
as their product.  -/
LinearOrderedCommGroupWithZero.inl : (α : Type u_1) →
  (β : Type u_2) →
    [inst : LinearOrderedCommGroupWithZero α] →
      [inst_1 : LinearOrderedCommGroupWithZero β] → α →*₀o WithZero (Lex (αˣ × βˣ))
-- Mathlib.RingTheory.AdjoinRoot
/-- The canonical algebraic equivalence between `AdjoinRoot p` and `AdjoinRoot g`,
where the two polynomials `f g : S[X]` are associated.  -/
AdjoinRoot.algEquivOfAssociated : (R : Type u_1) →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] → (f g : Polynomial S) → Associated f g → AdjoinRoot f ≃ₐ[R] AdjoinRoot g
-- Std.Http.Protocol.H1.Event
Std.Http.Protocol.H1.Event.failed.injEq : ∀ {dir : Std.Http.Protocol.H1.Direction} (err err_1 : Std.Http.Protocol.H1.Error),
  (Std.Http.Protocol.H1.Event.failed err = Std.Http.Protocol.H1.Event.failed err_1) = (err = err_1)
-- Mathlib.Topology.Compactness.CountablyCompact
/-- A set is countably compact if and only if every countable open cover has a finite subcover.  -/
isCountablyCompact_iff_countable_open_cover : ∀ {E : Type u_2} [inst : TopologicalSpace E] {A : Set E},
  IsCountablyCompact A ↔ ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen (U i)) → A ⊆ ⋃ i, U i → ∃ t, A ⊆ ⋃ i ∈ t, U i
-- Lean.Structure
/-- Data for a direct parent of a structure.
Some structure parents are represented as subobjects (embedded structures),
and for these the parent projection is a true projection.
If a structure parent shares a field with a previous parent, it will become an implicit parent,
and all the fields of the structure parent that do not occur in earlier parents are fields of the new structure
 -/
Lean.StructureParentInfo : Type
-- Mathlib.RingTheory.MatrixAlgebra
kroneckerTMulLinearEquiv_symm_kroneckerTMul : ∀ (l : Type u_1) (m : Type u_2) (n : Type u_3) (p : Type u_4) (R : Type u_5) (S : Type u_6) (M : Type u_9)
  (N : Type u_10) [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N]
  [inst_4 : Algebra R S] [inst_5 : Module R M] [inst_6 : Module S M] [inst_7 : Module R N]
  [inst_8 : IsScalarTower R S M] [inst_9 : Fintype l] [inst_10 : Fintype m] [inst_11 : Fintype n] [inst_12 : Fintype p]
  [inst_13 : DecidableEq l] [inst_14 : DecidableEq m] [inst_15 : DecidableEq n] [inst_16 : DecidableEq p]
  (a : Matrix l m M) (b : Matrix n p N),
  (kroneckerTMulLinearEquiv l m n p R S M N).symm (Matrix.kroneckerMap (TensorProduct.tmul R) a b) = a ⊗ₜ[R] b
-- Mathlib.Logic.Basic
forall₂_true_iff : ∀ {α : Sort u_1} {β : α → Sort u_3}, (∀ (a : α) (a : β a), True) ↔ True
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMultispan.instInhabitedOfL : {J : CategoryTheory.Limits.MultispanShape} → [Inhabited J.L] → Inhabited (CategoryTheory.Limits.WalkingMultispan J)
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.IsLocallyFiniteMeasure.mk : ∀ {α : Type u_1} {m0 : MeasurableSpace α} [inst : TopologicalSpace α] {μ : MeasureTheory.Measure α},
  (∀ (x : α), μ.FiniteAtFilter (nhds x)) → MeasureTheory.IsLocallyFiniteMeasure μ