mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.iterate_derivative_X_sub_pow_self : ∀ {R : Type u} [inst : CommRing R] (n : ℕ) (c : R),
  (⇑Polynomial.derivative)^[n] ((Polynomial.X - Polynomial.C c) ^ n) = ↑n.factorial
-- Std.Data.HashMap.Basic
/-- Returns an array of all keys present in the hash map in some order.  -/
Std.HashMap.keysArray : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → Array α
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
AddChar.complexBasis.congr_simp : ∀ (α : Type u_1) [inst : AddCommGroup α] [inst_1 : Finite α], AddChar.complexBasis α = AddChar.complexBasis α
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.Methods.mk.injEq : ∀ (pre post pre_1 post_1 : Lean.Meta.Sym.DSimp.DSimproc),
  ({ pre := pre, post := post } = { pre := pre_1, post := post_1 }) = (pre = pre_1 ∧ post = post_1)
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Iter.toIterM.eq_1 : ∀ {α β : Type w} (it : Std.Iter β), it.toIterM = { internalState := it.internalState }
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.unitsSMul_neg : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B}
  (u : ℤˣ) (w : HNNExtension.NormalWord d),
  HNNExtension.NormalWord.unitsSMul φ (-u) (HNNExtension.NormalWord.unitsSMul φ u w) = w
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
WithSeminorms.uniformEquicontinuous_iff_exists_continuous_seminorm : ∀ {𝕜 : Type u_2} {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} {ι' : Type u_10} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : NormedField 𝕜₂] [inst_4 : AddCommGroup F]
  [inst_5 : Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂] {κ : Type u_11} {q : SeminormFamily 𝕜₂ F ι'}
  [inst_7 : UniformSpace E] [IsUniformAddGroup E] [u : UniformSpace F] [IsUniformAddGroup F],
  WithSeminorms q →
    ∀ [ContinuousSMul 𝕜 E] (f : κ → E →ₛₗ[σ₁₂] F),
      UniformEquicontinuous (DFunLike.coe ∘ f) ↔ ∀ (i : ι'), ∃ p, Continuous ⇑p ∧ ∀ (k : κ), (q i).comp (f k) ≤ p
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.instFullHoCatToHoCat : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  HomotopicalAlgebra.FibrantObject.toHoCat.Full
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_insertMany_list : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List (α × β)},
  List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
    (∀ a ∈ t, (List.map Prod.fst l).contains a = false) → (t.insertMany l).size = t.size + l.length
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IsFractionRing.liftAlgHom.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_4} [inst_1 : CommRing A] {K : Type u_5} [inst_2 : Field K]
  {L : Type u_7} [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] [inst_6 : Algebra R A]
  [inst_7 : Algebra R K] [inst_8 : IsScalarTower R A K] [inst_9 : Algebra R L] {g g_1 : A →ₐ[R] L} (e_g : g = g_1)
  (hg : Function.Injective ⇑g), IsFractionRing.liftAlgHom hg = IsFractionRing.liftAlgHom ⋯
-- Mathlib.LinearAlgebra.Matrix.Invertible
/-- The **Woodbury Identity** (`⅟` version).

See `Matrix.invOf_add_mul_mul'` for the Binomial Inverse Theorem.  -/
Matrix.invOf_add_mul_mul : ∀ {m : Type u_1} {n : Type u_2} {α : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Fintype m]
  [inst_3 : DecidableEq m] [inst_4 : Ring α] (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α)
  [inst_5 : Invertible A] [inst_6 : Invertible C] [inst_7 : Invertible (⅟C + V * ⅟A * U)]
  [inst_8 : Invertible (A + U * C * V)], ⅟(A + U * C * V) = ⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
ContinuousOn.log : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℝ} {s : Set α},
  ContinuousOn f s → (∀ x ∈ s, f x ≠ 0) → ContinuousOn (fun x => Real.log (f x)) s
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Manifold.LiftSourceTargetPropertyAt.source_subset_preimage_source : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G}
  {M : Type u_10} {N : Type u_12} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop}
  (h : Manifold.LiftSourceTargetPropertyAt I J n f x P), h.domChart.source ⊆ f ⁻¹' h.codChart.source
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- The type of monoid homomorphisms satisfying the characteristic predicate: if `f : M →* N`
satisfies this predicate, then `N` is isomorphic to the localization of `M` at `S`.  -/
Submonoid.LocalizationMap : {M : Type u_1} → [inst : CommMonoid M] → Submonoid M → (N : Type u_2) → [CommMonoid N] → Type (max u_1 u_2)
-- Mathlib.Topology.Order.LawsonTopology
Topology.lawson_le_lower : ∀ {α : Type u_1} [inst : Preorder α], Topology.lawson α ≤ Topology.lower α
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
/-- The degree bound on a constructible set for Chevalley's theorem for the inclusion `R ↪ R[X]`.  -/
PrimeSpectrum.ConstructibleSetData.degBound : {R : Type u_1} → [inst : CommSemiring R] → PrimeSpectrum.ConstructibleSetData (Polynomial R) → ℕ
-- Mathlib.RingTheory.Kaehler.TensorProduct
KaehlerDifferential.tensorKaehlerEquivBase_symm_apply : ∀ (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] (a : Ω[B⁄S]),
  (KaehlerDifferential.tensorKaehlerEquivBase R S A B).symm a =
    (KaehlerDifferential.derivationTensorProduct R S A B).liftKaehlerDifferential a
-- Mathlib.Algebra.Lie.BaseChange
LieSubmodule.coe_baseChange : ∀ (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M]
  [inst_6 : LieModule R L M] [inst_7 : CommRing A] [inst_8 : Algebra R A] (N : LieSubmodule R L M),
  ↑(LieSubmodule.baseChange A N) = Submodule.baseChange A ↑N
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
_private.Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen.0.Convex.condExp_mem_of_hereditarilyLindelofSpace : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2} {f : α → E}
  {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set E} [MeasureTheory.IsFiniteMeasure μ]
  [HereditarilyLindelofSpace E],
  m ≤ mα →
    MeasureTheory.Integrable f μ → IsClosed s → Convex ℝ s → (∀ᵐ (a : α) ∂μ, f a ∈ s) → ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s
-- Mathlib.AlgebraicGeometry.Sites.Representability
AlgebraicGeometry.Scheme.GlueData.sheafValGluedMk.congr_simp : ∀ (D : AlgebraicGeometry.Scheme.GlueData) {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type v)}
  (s s_1 : (j : D.J) → F.obj.obj (Opposite.op (D.U j))) (e_s : s = s_1)
  (h :
    ∀ (i j : D.J),
      (CategoryTheory.ConcreteCategory.hom (F.obj.map (D.f i j).op)) (s i) =
        (CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.CategoryStruct.comp (D.f j i).op (D.t i j).op)))
          (s j)),
  D.sheafValGluedMk s h = D.sheafValGluedMk s_1 ⋯
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.ofHom_comp : ∀ (R : Type u) [inst : CommRing R] {X Y Z : Type v} [inst_1 : Ring X] [inst_2 : Ring Y] [inst_3 : Ring Z]
  [inst_4 : Algebra R X] [inst_5 : Algebra R Y] [inst_6 : Algebra R Z] (f : X →ₐ[R] Y) (g : Y →ₐ[R] Z),
  AlgCat.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (AlgCat.ofHom f) (AlgCat.ofHom g)
-- Mathlib.NumberTheory.Height.Basic
/-- The multiplicative height of a pointwise product of tuples is bounded by the product
of their multiplicative heights.  -/
Height.mulHeight_mul_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x y : ι → K),
  Height.mulHeight (x * y) ≤ Height.mulHeight x * Height.mulHeight y
-- Mathlib.Order.Hom.Lattice
/-- An `InfHomClass` morphism preserves infima.  -/
InfHomClass.map_inf : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} {inst : Min α} {inst_1 : Min β} {inst_2 : FunLike F α β}
  [self : InfHomClass F α β] (f : F) (a b : α), f (a ⊓ b) = f a ⊓ f b
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ \ t₂).getKey! k = t₁.getKey! k
-- Mathlib.Analysis.Analytic.CPolynomialDef
HasFiniteFPowerSeriesAt.of_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {m n : ℕ},
  HasFiniteFPowerSeriesAt f p x n → n ≤ m → HasFiniteFPowerSeriesAt f p x m
-- Mathlib.Order.Category.BddDistLat
BddDistLat.isBoundedOrder : (self : BddDistLat) → BoundedOrder ↑self.toDistLat
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
CategoryTheory.Limits.weakLimit.pullbackConeFst_cone_cospan : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasWeakLimit (CategoryTheory.Limits.cospan f g)],
  CategoryTheory.Limits.PullbackCone.fst (CategoryTheory.Limits.weakLimit.cone (CategoryTheory.Limits.cospan f g)) =
    CategoryTheory.Limits.weakPullback.fst f g
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
IsCyclotomicExtension.Rat.galEquivZMod_stabilizer : ∀ (n : ℕ) [inst : NeZero n] (K : Type u_1) [inst_1 : Field K] [inst_2 : NumberField K]
  [hK : IsCyclotomicExtension {n} ℚ K] (p : ℕ) [hp : Fact (Nat.Prime p)] (P : Ideal (NumberField.RingOfIntegers K))
  [P.IsMaximal] [P.LiesOver (Ideal.span {↑p})] (hn : p.Coprime n),
  (IsCyclotomicExtension.Rat.galEquivZMod n K).mapSubgroup (MulAction.stabilizer Gal(K/ℚ) P) =
    Subgroup.zpowers (ZMod.unitOfCoprime p hn)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.fold_eq_foldl_toList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {δ : Type w} {β : Type v} {m : Std.DHashMap.Raw α fun x => β},
  m.WF →
    ∀ {f : δ → α → β → δ} {init : δ},
      Std.DHashMap.Raw.fold f init m = List.foldl (fun a b => f a b.1 b.2) init (Std.DHashMap.Raw.Const.toList m)
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.Theorem.lam.inj : ∀ {thm thm_1 : Mathlib.Meta.FunProp.LambdaTheorem},
  Mathlib.Meta.FunProp.Theorem.lam thm = Mathlib.Meta.FunProp.Theorem.lam thm_1 → thm = thm_1
-- Lean.Meta.Sym.SynthInstance
/-- Helper function for instantiating a type class `type`, and
then using the result to perform `isDefEq x val`.
 -/
Lean.Meta.Sym.synthInstanceAndAssign : Lean.Expr → Lean.Expr → Lean.Meta.Sym.SymM Bool
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.ext_iff : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] {χ χ' : MulChar R R'},
  χ = χ' ↔ ∀ (a : Rˣ), χ ↑a = χ' ↑a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.leftUnitor_hom_left_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {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}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') (X : A),
  φ.leftUnitor.hom.left.app X = CategoryTheory.CategoryStruct.id (φ.left.obj X)
-- Mathlib.Data.Finset.Card
Finset.card_filter_le_iff : ∀ {α : Type u_1} (s : Finset α) (P : α → Prop) [inst : DecidablePred P] (n : ℕ),
  (Finset.filter P s).card ≤ n ↔ ∀ s' ⊆ s, n < s'.card → ∃ a ∈ s', ¬P a
-- Lean.Parser.Term
/-- Configuration options for `let` tactics.  -/
Lean.Parser.Term.letConfig : Lean.Parser.Parser
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.supportedEquivFinsupp.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  (s : Set M),
  MonoidAlgebra.supportedEquivFinsupp s =
    { toFun := fun x => ⟨(↑x).coeff, ⋯⟩, map_add' := ⋯, map_smul' := ⋯,
        invFun := fun x => ⟨MonoidAlgebra.ofCoeff ↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } ≪≫ₗ
      Finsupp.supportedEquivFinsupp s
-- Mathlib.ModelTheory.Algebra.Field.Basic
/-- The first-order sentence corresponding to each field axiom  -/
FirstOrder.Field.FieldAxiom.toSentence : FirstOrder.Field.FieldAxiom → FirstOrder.Language.ring.Sentence
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_modify_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  [inst_1 : Inhabited (β k)] {f : β k → β k}, (m.modify k f).get! k = (Option.map f (m.get? k)).get!
-- Init.Data.UInt.Bitwise
UInt8.zero_xor : ∀ {a : UInt8}, 0 ^^^ a = a
-- Mathlib.Analysis.Convex.Strict
strictConvex_iff_ordConnected : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜] {s : Set 𝕜}, StrictConvex 𝕜 s ↔ s.OrdConnected
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.contains_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  (Std.DTreeMap.Const.unitOfList l cmp).contains k = l.contains k
-- Mathlib.Data.NNReal.Defs
NNReal.instSemiring : Semiring NNReal
-- Lean.Elab.Parallel
/-- Runs a list of TacticM computations in parallel and returns the first successful result
(by completion order, not list order).

If `cancel := true` (the default), cancels all remaining tasks after the first success.
 -/
Lean.Elab.Tactic.TacticM.parFirst : {α : Type} → List (Lean.Elab.Tactic.TacticM α) → optParam Bool true → Lean.Elab.Tactic.TacticM α
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Path.Homotopy.trans_refl_reparam : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x₀ x₁ : X} (p : Path x₀ x₁),
  p.trans (Path.refl x₁) =
    p.reparam (fun t => ⟨Path.Homotopy.transReflReparamAux t, ⋯⟩) Path.Homotopy.trans_refl_reparam._proof_1 ⋯ ⋯
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_union : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α} {fallback : β},
  Std.DTreeMap.Const.getD (t₁ ∪ t₂) k fallback = Std.DTreeMap.Const.getD t₂ k (Std.DTreeMap.Const.getD t₁ k fallback)
-- Mathlib.Data.Finset.Lattice.Basic
Finset.subset_union_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s₁ s₂ : Finset α}, s₂ ⊆ s₁ ∪ s₂
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
IsPurelyInseparable.hasExponent_iff : ∀ (K : Type u_2) (L : Type u_3) [inst : CommRing K] [inst_1 : Ring L] [inst_2 : Algebra K L],
  IsPurelyInseparable.HasExponent K L ↔ ∃ e, ∀ (a : L), a ^ ringExpChar K ^ e ∈ (algebraMap K L).range
-- Std.Data.Iterators.Consumers.Monadic.Set
/-- Traverses the given iterator and stores the emitted values in a {name}`ExtTreeSet`.

If the iterator is not finite, this function might run forever. Given {givenInstance}`Finite α m`,
the variant {lean}`it.ensureTermination.toExtTreeSet cmp` always terminates after finitely
many steps.
 -/
Std.IterM.toExtTreeSet : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m m] →
          Std.IterM m β →
            (cmp : autoParam (β → β → Ordering) Std.IterM.toExtTreeSet._auto_1) →
              [Std.TransCmp cmp] → m (Std.ExtTreeSet β cmp)
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.isDynNetIn_singleton : ∀ {X : Type u_1} {F : Set X} {x : X} (T : X → X) (U : SetRel X X) (n : ℕ), x ∈ F → Dynamics.IsDynNetIn T F U n {x}
-- Mathlib.RingTheory.MvPolynomial.Localization
_private.Mathlib.RingTheory.MvPolynomial.Localization.0.IsLocalization.Away.auxInv : {R : Type u_2} →
  [inst : CommRing R] →
    (S : Type u_3) →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (r : R) →
            [IsLocalization.Away r S] →
              S →+* MvPolynomial Unit R ⧸ Ideal.span {MvPolynomial.C r * MvPolynomial.X () - 1}
-- Init.Data.SInt.Bitwise
instLawfulCommIdentityInt16HOrOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 ||| x2) 0
-- Init.Data.List.Monadic
List.mapM_unattach : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {P : α → Prop}
  {xs : List (Subtype P)} {f : α → m β},
  List.mapM f xs.unattach =
    List.mapM
      (fun x =>
        match x with
        | ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (f (wfParam x))))
      xs
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castSucc_Iio_castSucc : ∀ {n : ℕ} (i : Fin n), Fin.castSucc ⁻¹' Set.Iio i.castSucc = Set.Iio i
-- Mathlib.Data.List.OfFn
List.getLast_ofFn_succ : ∀ {α : Type u} {n : ℕ} (f : Fin n.succ → α), (List.ofFn f).getLast ⋯ = f (Fin.last n)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.maxKeyD.match_1.eq_3 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → α → Sort u_3) (size : ℕ) (k : α)
  (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1)
  (l_1 r : Std.DTreeMap.Internal.Impl α β) (fallback : α)
  (h_1 : (fallback : α) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (x : α) → motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (size_2 : ℕ) →
              (k_2 : α) →
                (v_2 : β k_2) →
                  (l_2 r_1 : Std.DTreeMap.Internal.Impl α β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1 →
                      (fallback : α) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1))
                          fallback),
  (match Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r),
      fallback with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_2 size k v l x
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1),
      fallback => h_3 size k v l r size_2 k_2 v_2 l_2 r_1 h fallback) =
    h_3 size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) size_1 k_1 v_1 l_1 r ⋯ fallback
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.regular.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A : C)
  [inst_2 : CategoryTheory.MonObj A], CategoryTheory.Mod.regular A = { X := A, mod := CategoryTheory.ModObj.regular A }
-- Mathlib.Data.Matrix.Diagonal
/-- The diagonal of a square matrix.  -/
Matrix.diag : {n : Type u_3} → {α : Type v} → Matrix n n α → n → α
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.instReprFunIndParamKind : Repr Lean.Meta.FunIndParamKind
-- Mathlib.Data.Set.Disjoint
Disjoint.union_right : ∀ {α : Type u_1} {s t u : Set α}, Disjoint s t → Disjoint s u → Disjoint s (t ∪ u)
-- Init.Data.Option.Lemmas
Option.get_mem : ∀ {α : Type u_1} {o : Option α} (h : o.isSome = true), o.get h ∈ o
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
Seminorm.abs_le_of_le : ∀ {E : Type u_6} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {p : Seminorm ℝ E} {f : E →ₗ[ℝ] ℝ},
  (∀ (x : E), f x ≤ p x) → ∀ (x : E), |f x| ≤ p x
-- Mathlib.Analysis.Analytic.Constructions
/-- Finite sums of analytic functions are analytic  -/
Finset.analyticAt_sum : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {f : α → E → F} {c : E} (N : Finset α), (∀ n ∈ N, AnalyticAt 𝕜 (f n) c) → AnalyticAt 𝕜 (∑ n ∈ N, f n) c
-- Mathlib.Topology.Metrizable.Basic
/-- If a set `s` is separable, then the corresponding subtype is separable in a
pseudo metrizable space.
This is not obvious, as the countable set whose closure covers `s` does not need in
general to be contained in `s`.  -/
TopologicalSpace.IsSeparable.separableSpace : ∀ {X : Type u_2} [inst : TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] {s : Set X},
  TopologicalSpace.IsSeparable s → TopologicalSpace.SeparableSpace ↑s
-- Mathlib.Order.Atoms
bot_covBy_top : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [IsSimpleOrder α], ⊥ ⋖ ⊤
-- Mathlib.Algebra.Field.IsField
not_isField_of_subsingleton : ∀ (R : Type u) [inst : Semiring R] [Subsingleton R], ¬IsField R
-- Mathlib.Algebra.Category.ModuleCat.Stalk
CategoryTheory.Limits.IsColimit.ι_smul : ∀ {C : Type u_1} [inst : CategoryTheory.SmallCategory C] [inst_1 : CategoryTheory.IsFiltered C]
  (R : CategoryTheory.Functor C RingCat) (M : CategoryTheory.Functor C Ab)
  [inst_2 : (i : C) → Module ↑(R.obj i) ↑(M.obj i)]
  (H :
    ∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
      (CategoryTheory.ConcreteCategory.hom (M.map f)) (r • m) =
        (CategoryTheory.ConcreteCategory.hom (R.map f)) r • (CategoryTheory.ConcreteCategory.hom (M.map f)) m)
  {cR : CategoryTheory.Limits.Cocone R} (hcR : CategoryTheory.Limits.IsColimit cR) {cM : CategoryTheory.Limits.Cocone M}
  (hcM : CategoryTheory.Limits.IsColimit cM) (i : C) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
  (CategoryTheory.ConcreteCategory.hom (cM.ι.app i)) (r • m) =
    (CategoryTheory.ConcreteCategory.hom (cR.ι.app i)) r • (CategoryTheory.ConcreteCategory.hom (cM.ι.app i)) m
-- Init.Data.Iterators.Internal.LawfulMonadLiftFunction
Std.Internal.instLawfulMonadLiftFunctionId : ∀ {m : Type u → Type v} [inst : Monad m], Std.Internal.LawfulMonadLiftFunction fun ⦃α⦄ => id
-- Mathlib.Analysis.SpecialFunctions.Artanh
/-- `Real.tanh` as a `PartialEquiv`.  -/
Real.tanhPartialEquiv : PartialEquiv ℝ ℝ
-- Mathlib.Algebra.DirectSum.Ring
/-- The `IntCast` instance on `A 0`, given `GRing A`.  -/
DirectSum.instIntCastOfNat : {ι : Type u_1} →
  (A : ι → Type u_2) →
    [inst : (i : ι) → AddCommGroup (A i)] → [inst_1 : AddMonoid ι] → [DirectSum.GRing A] → IntCast (A 0)
-- Mathlib.Algebra.Category.Grp.Zero
AddCommGrpCat.subsingleton_of_isZero : ∀ {G : AddCommGrpCat}, CategoryTheory.Limits.IsZero G → Subsingleton ↑G
-- Mathlib.Algebra.Regular.Prod
IsLeftRegular.prodMk : ∀ {R : Type u_2} {S : Type u_3} [inst : Mul R] [inst_1 : Mul S] {a : R} {b : S},
  IsLeftRegular a → IsLeftRegular b → IsLeftRegular (a, b)
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_17 : HSub Std.Time.Second.Offset Std.Time.Week.Offset Std.Time.Second.Offset