mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.mk.inj : ∀ {E : Type u_2} {F : Type u_3} {inst : NormedAddCommGroup E} {inst_1 : NormedSpace ℝ E} {inst_2 : NormedAddCommGroup F}
  {inst_3 : NormedSpace ℝ F} {n : ℕ∞} {K : TopologicalSpace.Compacts E} {toFun : E → F}
  {contDiff' : ContDiff ℝ (↑n) toFun} {zero_on_compl' : Set.EqOn toFun 0 (↑K)ᶜ} {toFun_1 : E → F}
  {contDiff'_1 : ContDiff ℝ (↑n) toFun_1} {zero_on_compl'_1 : Set.EqOn toFun_1 0 (↑K)ᶜ},
  { toFun := toFun, contDiff' := contDiff', zero_on_compl' := zero_on_compl' } =
      { toFun := toFun_1, contDiff' := contDiff'_1, zero_on_compl' := zero_on_compl'_1 } →
    toFun = toFun_1
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.curriedAssociatorNatIso_hom_app_app_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X X_1 X_2 : C),
  (((CategoryTheory.MonoidalCategory.curriedAssociatorNatIso C).hom.app X).app X_1).app X_2 =
    (CategoryTheory.MonoidalCategoryStruct.associator X X_1 X_2).hom
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonDocumentSelector : Lean.ToJson Lean.Lsp.DocumentSelector
-- Std.Http.Data.Status
/-- 422 Unprocessable Entity
 -/
Std.Http.Status.unprocessableEntity : Std.Http.Status
-- Mathlib.FieldTheory.IsSepClosed
IsSepClosure.mk : ∀ {k : Type u} [inst : Field k] {K : Type v} [inst_1 : Field K] [inst_2 : Algebra k K],
  IsSepClosed K → Algebra.IsSeparable k K → IsSepClosure k K
-- Init.Data.Nat.Bitwise.Lemmas
Nat.bitwise_mul_two_pow : ∀ {f : Bool → Bool → Bool} {x y n : ℕ},
  autoParam (f false false = false) Nat.bitwise_mul_two_pow._auto_9 →
    Nat.bitwise f x y * 2 ^ n = Nat.bitwise f (x * 2 ^ n) (y * 2 ^ n)
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.left_of_add_measure : ∀ {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : ENorm ε] {f : α → ε},
  MeasureTheory.HasFiniteIntegral f (μ + ν) → MeasureTheory.HasFiniteIntegral f μ
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.polar_self : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticMap R M N) (x : M), QuadraticMap.polar (⇑Q) x x = 2 • Q x
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.gaussianReal_apply_eq_integral : ∀ (μ : ℝ) {v : NNReal},
  v ≠ 0 →
    ∀ (s : Set ℝ),
      (ProbabilityTheory.gaussianReal μ v) s = ENNReal.ofReal (∫ (x : ℝ) in s, ProbabilityTheory.gaussianPDFReal μ v x)
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- Notation for sections of a presheaf of module.  -/
AlgebraicGeometry.«termΓ(_,_)_1» : Lean.ParserDescr
-- Init.Data.Array.Find
Array.findIdx?_singleton : ∀ {α : Type u_1} {a : α} {p : α → Bool}, Array.findIdx? p #[a] = if p a = true then some 0 else none
-- Init.Data.UInt.Lemmas
UInt32.toUInt64_toUSize : ∀ (n : UInt32), n.toUSize.toUInt64 = n.toUInt64
-- Mathlib.ModelTheory.Fraisse
FirstOrder.Language.Hereditary.is_equiv_invariant_of_fg : ∀ {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)},
  FirstOrder.Language.Hereditary K →
    (∀ M ∈ K, FirstOrder.Language.Structure.FG L ↑M) →
      ∀ (M N : CategoryTheory.Bundled L.Structure), Nonempty (L.Equiv ↑M ↑N) → (M ∈ K ↔ N ∈ K)
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
/-- If `I^2 = 0`, then `I` admits a divided power structure.  -/
DividedPowers.OfSquareZero.dividedPowers : {A : Type u_1} → [inst : CommSemiring A] → {I : Ideal A} → [DecidablePred fun x => x ∈ I] → I ^ 2 = 0 → DividedPowers I
-- Mathlib.ModelTheory.Syntax
/-- The representation of a function symbol as a term, on fresh variables indexed by Fin.  -/
FirstOrder.Language.Functions.term : {L : FirstOrder.Language} → {n : ℕ} → L.Functions n → L.Term (Fin n)
-- Mathlib.Data.ENNReal.Operations
ENNReal.toReal_sSup : ∀ (s : Set ENNReal), (∀ r ∈ s, r ≠ ⊤) → (sSup s).toReal = sSup (ENNReal.toReal '' s)
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
/-- Auxiliary definition for `equivalence`.  -/
SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompFunctorIso : (X Y : SSet.Truncated 2) →
  (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).comp
      (SSet.Truncated.HomotopyCategory.BinaryProduct.functor X Y) ≅
    CategoryTheory.Functor.id (X.HomotopyCategory × Y.HomotopyCategory)
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.toFun_neg : ∀ {R : Type u} [inst : CommRing R] {M : Type u_6} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_7}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M →ₚₗ[R] N) (S : Type u_8) [inst_5 : CommSemiring S]
  [inst_6 : Algebra R S], PolynomialLaw.toFun S (-f) = -1 • PolynomialLaw.toFun S f
-- Mathlib.Analysis.Fourier.Notation
FourierTransform.fourierₗ_apply : ∀ {R : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid E] [inst_2 : AddCommMonoid F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : FourierTransform E F] [inst_6 : FourierAdd E F]
  [inst_7 : FourierSMul R E F] (f : E), (FourierTransform.fourierₗ R E) f = FourierTransform.fourier f
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {fallback : β k}, k ∉ m₂ → (m₁ ∪ m₂).getD k fallback = m₁.getD k fallback
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.K'.elim.eq_4 : ∀ (a b c d : List Turing.PartrecToTM2.Γ'), Turing.PartrecToTM2.K'.elim a b c d Turing.PartrecToTM2.K'.stack = d
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
/-- The diagram over all `{ V : Opens X // ∃ i, V ≤ U i }` is a limit iff the diagram
over `U i` and `U i ⊓ U j` is a limit.  -/
TopCat.Presheaf.isLimitOpensLeCoverEquivPairwise : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : TopCat} →
      (F : TopCat.Presheaf C X) →
        {ι : Type u_2} →
          (U : ι → TopologicalSpace.Opens ↑X) →
            CategoryTheory.Limits.IsLimit
                (CategoryTheory.Functor.mapCone F (TopCat.Presheaf.SheafCondition.opensLeCoverCocone U).op) ≃
              CategoryTheory.Limits.IsLimit (CategoryTheory.Functor.mapCone F (CategoryTheory.Pairwise.cocone U).op)
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.toZeroHom : {G : Type u_6} → [inst : AddGroup G] → NonarchAddGroupSeminorm G → ZeroHom G ℝ
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.skyscraperSheafFunctor_map_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasProducts A] {X Y : A}
  (f : X ⟶ Y), (Φ.skyscraperSheafFunctor.map f).hom = Φ.skyscraperPresheafFunctor.map f
-- Init.Data.String.Lemmas.Pattern.Split.Basic
String.split_eq_split_toSlice : ∀ {ρ : Type} {pat : ρ} {σ : String.Slice → Type} [inst : String.Slice.Pattern.ToForwardSearcher pat σ]
  [inst_1 : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] {s : String},
  s.split pat = s.toSlice.split pat
-- Mathlib.Topology.Irreducible
IrreducibleSpace.isIrreducible_univ : ∀ (X : Type u_3) [inst : TopologicalSpace X] [IrreducibleSpace X], IsIrreducible Set.univ
-- Init.Data.Vector.Lemmas
Vector.mem_flatMap_of_mem : ∀ {β : Type u_1} {α : Type u_2} {n m : ℕ} {b : β} {xs : Vector α n} {f : α → Vector β m} {a : α},
  a ∈ xs → b ∈ f a → b ∈ xs.flatMap f
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.quot_out : ∀ {M : Type u_1} [inst : Monoid M] (a : Associates M), Associates.mk (Quot.out a) = a
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct
SSet.anodyneExtensions_pushoutObjObjι : ∀ {X₁ X₂ Y₁ Y₂ : SSet} {i : X₁ ⟶ Y₁} {j : X₂ ⟶ Y₂}
  (sq₁₂ : (CategoryTheory.MonoidalCategory.curriedTensor SSet).PushoutObjObj i j) [CategoryTheory.Mono i],
  SSet.anodyneExtensions j → SSet.anodyneExtensions sq₁₂.ι
-- Mathlib.Tactic.Linter.FlexibleLinter
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.TacticData.mk.injEq : ∀ (stx : Lean.Syntax) (ci : Lean.Elab.ContextInfo) (mctxBefore mctxAfter : Lean.MetavarContext)
  (goalsTargetedBy goalsCreatedBy : List Lean.MVarId) (stx_1 : Lean.Syntax) (ci_1 : Lean.Elab.ContextInfo)
  (mctxBefore_1 mctxAfter_1 : Lean.MetavarContext) (goalsTargetedBy_1 goalsCreatedBy_1 : List Lean.MVarId),
  ({ stx := stx, ci := ci, mctxBefore := mctxBefore, mctxAfter := mctxAfter, goalsTargetedBy := goalsTargetedBy,
        goalsCreatedBy := goalsCreatedBy } =
      { stx := stx_1, ci := ci_1, mctxBefore := mctxBefore_1, mctxAfter := mctxAfter_1,
        goalsTargetedBy := goalsTargetedBy_1, goalsCreatedBy := goalsCreatedBy_1 }) =
    (stx = stx_1 ∧
      ci = ci_1 ∧
        mctxBefore = mctxBefore_1 ∧
          mctxAfter = mctxAfter_1 ∧ goalsTargetedBy = goalsTargetedBy_1 ∧ goalsCreatedBy = goalsCreatedBy_1)
-- Aesop.Builder.Apply
Aesop.RuleBuilder.getApplyIndexingMode : Lean.Meta.TransparencyMode → Lean.Expr → Lean.MetaM Aesop.IndexingMode
-- Mathlib.FieldTheory.Laurent
RatFunc.laurent_X : ∀ {R : Type u} [inst : CommRing R] (r : R) [inst_1 : IsDomain R],
  (RatFunc.laurent r) RatFunc.X = RatFunc.X + RatFunc.C r
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.add_comp : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] (ρ : Representation A G V) (σ : Representation A G W)
  (τ : Representation A G U) (f : σ.IntertwiningMap τ) (g₁ g₂ : ρ.IntertwiningMap σ),
  f.comp (g₁ + g₂) = f.comp g₁ + f.comp g₂
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
/-- The invariant vector field associated to a vector `v` in the Lie algebra. At a point `g`, it
is given by the image of `v` under left-multiplication by `g`.  -/
mulInvariantVectorField : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {H : Type u_2} →
      [inst_1 : TopologicalSpace H] →
        {E : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : NormedSpace 𝕜 E] →
              {I : ModelWithCorners 𝕜 E H} →
                {G : Type u_4} →
                  [inst_4 : TopologicalSpace G] →
                    [inst_5 : ChartedSpace H G] → [inst_6 : Group G] → GroupLieAlgebra I G → (g : G) → TangentSpace I g
-- Mathlib.Algebra.Category.Grp.Limits
/-- An auxiliary declaration to speed up typechecking.  -/
CommGrpCat.forget₂CommMon_preservesLimitsAux : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J CommGrpCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommGrpCat)).sections] →
        CategoryTheory.Limits.IsLimit ((CategoryTheory.forget₂ CommGrpCat CommMonCat).mapCone (CommGrpCat.limitCone F))
-- Mathlib.Control.Random
/-- Generate a random `Bool`.  -/
Random.randBool : {m : Type → Type u_1} → [Monad m] → {g : Type} → [RandomGen g] → RandGT g m Bool
-- Init.Core
PNonScalar.mk.inj : ∀ {v v_1 : ℕ}, PNonScalar.mk v = PNonScalar.mk v_1 → v = v_1
-- Mathlib.Data.Multiset.Pairwise
Multiset.Pairwise.forall : ∀ {α : Type u_1} {r : α → α → Prop} {s : Multiset α} [Std.Symm r],
  Multiset.Pairwise r s → ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a ≠ b → r a b
-- Lean.Attributes
Lean.EnumAttributes.getValue : {α : Type} → [Inhabited α] → Lean.EnumAttributes α → Lean.Environment → Lean.Name → Option α
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.instConcreteCategoryBialgHomCarrier : {R : Type u} → [inst : CommRing R] → CategoryTheory.ConcreteCategory (CommBialgCat R) fun x1 x2 => ↑x1 →ₐc[R] ↑x2
-- Mathlib.MeasureTheory.Function.LpSpace.Complete
MeasureTheory.Lp.completeSpace_lp_of_cauchy_complete_eLpNorm : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {E : Type u_3}
  [inst : NormedAddCommGroup E] [hp : Fact (1 ≤ p)],
  (∀ (f : ℕ → α → E),
      (∀ (n : ℕ), MeasureTheory.MemLp (f n) p μ) →
        ∀ (B : ℕ → ENNReal),
          ∑' (i : ℕ), B i < ⊤ →
            (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → MeasureTheory.eLpNorm (f n - f m_1) p μ < B N) →
              ∃ f_lim,
                MeasureTheory.MemLp f_lim p μ ∧
                  Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - f_lim) p μ) Filter.atTop (nhds 0)) →
    CompleteSpace ↥(MeasureTheory.Lp E p μ)
-- Mathlib.GroupTheory.OrderOfElement
nsmul_inj_mod : ∀ {G : Type u_1} [inst : AddLeftCancelMonoid G] {x : G} {n m : ℕ}, n • x = m • x ↔ n % addOrderOf x = m % addOrderOf x
-- Mathlib.Algebra.Ring.Defs
NonUnitalNonAssocRing.toHasDistribNeg : {α : Type u} → [inst : NonUnitalNonAssocRing α] → HasDistribNeg α
-- Mathlib.Probability.UniformOn
ProbabilityTheory.uniformOn_of_univ : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω},
  s.Finite → s.Nonempty → (ProbabilityTheory.uniformOn s) Set.univ = 1
-- Mathlib.Tactic.TacticAnalysis
/-- Each tactic analysis round is represented by the declaration name for the `Config`.  -/
Mathlib.TacticAnalysis.Entry : Type
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.single_eq_zero : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {r : R} {m : M}, MonoidAlgebra.single m r = 0 ↔ r = 0
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.instIsIsoMapCochainComplexIntQOfQuasiIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {K L : CochainComplex C ℤ} (f : K ⟶ L) [QuasiIso f],
  CategoryTheory.IsIso (DerivedCategory.Q.map f)
-- Mathlib.Topology.EMetricSpace.Weak
instEDistOnePoint : {α : Type u} → [EDist α] → EDist (OnePoint α)
-- Mathlib.Topology.Separation.Hausdorff
SeparatedNhds.of_isCompact_isCompact : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] {s t : Set X},
  IsCompact s → IsCompact t → Disjoint s t → SeparatedNhds s t
-- Lean.Meta.Sym.SymM
/-- Auxiliary function for implementing `unfoldReducible` and `unfoldReducibleSimproc`.
Performs a single step.
 -/
Lean.Meta.Sym.unfoldReducibleStep : Lean.Expr → Lean.MetaM Lean.TransformStep
-- Init.Classical
Classical.not_forall_not : ∀ {α : Sort u_1} {p : α → Prop}, (¬∀ (x : α), ¬p x) ↔ ∃ x, p x
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.Subobject.Classifier.truth_as_subobject`.

---

The subobject of `𝒞.Ω` corresponding to the `truth` morphism.  -/
CategoryTheory.Classifier.truth_as_subobject : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → (𝒞 : CategoryTheory.Subobject.Classifier C) → CategoryTheory.Subobject 𝒞.Ω
-- Mathlib.Data.Fintype.Sets
Set.filter_mem_univ_eq_toFinset : ∀ {α : Type u_1} [inst : Fintype α] (s : Set α) [inst_1 : Fintype ↑s] [inst_2 : DecidablePred fun x => x ∈ s],
  {x | x ∈ s} = s.toFinset
-- Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
/-- If an `L^p` space is complete and nontrivial, then the target space is complete.  -/
MeasureTheory.completeSpace_of_completeSpace_Lp : ∀ {α : Type u_1} (E : Type u_2) [inst : NormedAddCommGroup E] {mα : MeasurableSpace α} (p : ENNReal)
  (μ : MeasureTheory.Measure α) [NormedSpace ℝ E] [hp : Fact (1 ≤ p)] [CompleteSpace ↥(MeasureTheory.Lp E p μ)]
  [Nontrivial ↥(MeasureTheory.Lp E p μ)], CompleteSpace E
-- Mathlib.Control.Traversable.Instances
Sum.instLawfulTraversable : ∀ {σ : Type u}, LawfulTraversable (Sum σ)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetDecl.mk.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (binderName : Lean.Name) (type : Lean.Expr)
  (value : Lean.Compiler.LCNF.LetValue pu) (fvarId_1 : Lean.FVarId) (binderName_1 : Lean.Name) (type_1 : Lean.Expr)
  (value_1 : Lean.Compiler.LCNF.LetValue pu),
  ({ fvarId := fvarId, binderName := binderName, type := type, value := value } =
      { fvarId := fvarId_1, binderName := binderName_1, type := type_1, value := value_1 }) =
    (fvarId = fvarId_1 ∧ binderName = binderName_1 ∧ type = type_1 ∧ value = value_1)
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
PartialDiffeomorph.mk.inj : ∀ {𝕜 : 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} {H₁ : Type u_5}
  {inst_5 : TopologicalSpace H₁} {H₂ : Type u_6} {inst_6 : TopologicalSpace H₂} {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} {inst_7 : TopologicalSpace M} {inst_8 : ChartedSpace H₁ M} {N : Type u_9}
  {inst_9 : TopologicalSpace N} {inst_10 : ChartedSpace H₂ N} {n : WithTop ℕ∞} {toPartialEquiv : PartialEquiv M N}
  {open_source : IsOpen toPartialEquiv.source} {open_target : IsOpen toPartialEquiv.target}
  {contMDiffOn_toFun : ContMDiffOn I J n (↑toPartialEquiv) toPartialEquiv.source}
  {contMDiffOn_invFun : ContMDiffOn J I n toPartialEquiv.invFun toPartialEquiv.target}
  {toPartialEquiv_1 : PartialEquiv M N} {open_source_1 : IsOpen toPartialEquiv_1.source}
  {open_target_1 : IsOpen toPartialEquiv_1.target}
  {contMDiffOn_toFun_1 : ContMDiffOn I J n (↑toPartialEquiv_1) toPartialEquiv_1.source}
  {contMDiffOn_invFun_1 : ContMDiffOn J I n toPartialEquiv_1.invFun toPartialEquiv_1.target},
  { toPartialEquiv := toPartialEquiv, open_source := open_source, open_target := open_target,
        contMDiffOn_toFun := contMDiffOn_toFun, contMDiffOn_invFun := contMDiffOn_invFun } =
      { toPartialEquiv := toPartialEquiv_1, open_source := open_source_1, open_target := open_target_1,
        contMDiffOn_toFun := contMDiffOn_toFun_1, contMDiffOn_invFun := contMDiffOn_invFun_1 } →
    toPartialEquiv = toPartialEquiv_1
-- Lean.Util.MonadCache
Lean.MonadStateCacheT.instMonad : {α β : Type} →
  {m : Type → Type} → [inst : BEq α] → [inst_1 : Hashable α] → [Monad m] → Monad (Lean.MonadStateCacheT α β m)
-- Lean.Message
/-- Simply formats the name.
See `MessageData.ofConstName` for richer messages.
 -/
Lean.MessageData.ofName : Lean.Name → Lean.MessageData
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.GRing.mk : {ι : Type u_1} →
  {A : ι → Type u_2} →
    [inst : AddMonoid ι] →
      [inst_1 : (i : ι) → AddCommGroup (A i)] →
        [toGSemiring : DirectSum.GSemiring A] →
          (intCast : ℤ → A 0) →
            (∀ (n : ℕ), intCast ↑n = DirectSum.GSemiring.natCast n) →
              (∀ (n : ℕ), intCast (Int.negSucc n) = -DirectSum.GSemiring.natCast (n + 1)) → DirectSum.GRing A
-- Mathlib.Logic.Equiv.List
/-- If `α` is encodable, then so is `List α`. This uses the `pair` and `unpair` functions from
`Data.Nat.Pairing`.  -/
List.encodable : {α : Type u_1} → [Encodable α] → Encodable (List α)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_eq_isSome_getKey? : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {a : α}, m.contains a = (m.getKey? a).isSome
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.hasFiniteIntegral_const : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  [MeasureTheory.IsFiniteMeasure μ] (c : β), MeasureTheory.HasFiniteIntegral (fun x => c) μ
-- Mathlib.Algebra.Category.Ring.Basic
RingEquiv.toRingCatIso_hom : ∀ {R S : Type u} [inst : Ring R] [inst_1 : Ring S] (e : R ≃+* S), e.toRingCatIso.hom = RingCat.ofHom ↑e
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatMkOfKerLERange.congr_simp : ∀ {R : Type u} [inst : Ring R] {X₁ X₂ X₃ : ModuleCat R} (f f_1 : X₁ ⟶ X₂) (e_f : f = f_1) (g g_1 : X₂ ⟶ X₃)
  (e_g : g = g_1) (hfg : (ModuleCat.Hom.hom f).range ≤ (ModuleCat.Hom.hom g).ker),
  CategoryTheory.ShortComplex.moduleCatMkOfKerLERange f g hfg =
    CategoryTheory.ShortComplex.moduleCatMkOfKerLERange f_1 g_1 ⋯
-- Mathlib.Data.W.Constructions
WType.instInhabitedListα : (γ : Type u) → Inhabited (WType.Listα γ)
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.HomRel.CompClosure.of : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {r : HomRel C} {a b : C} {m₁ m₂ : a ⟶ b},
  r m₁ m₂ → CategoryTheory.HomRel.CompClosure r m₁ m₂
-- Lean.Parser.Module
Lean.Parser.instInhabitedModuleParserState.default : Lean.Parser.ModuleParserState
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTreeTarget.mk.injEq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {w len : ℕ} (x : aig.RefVec (len * w))
  (h : 0 < len) (len_1 : ℕ) (x_1 : aig.RefVec (len_1 * w)) (h_1 : 0 < len_1),
  ({ len := len, x := x, h := h } = { len := len_1, x := x_1, h := h_1 }) = (len = len_1 ∧ x ≍ x_1)
-- Mathlib.Tactic.Attr.Register
/-- Simp set for `functor_norm`  -/
Parser.Attr.monad_norm : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getKeyLE : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      [Std.TransOrd α] →
        (k : α) → (t : Std.DTreeMap.Internal.Impl α β) → t.Ordered → (∃ a ∈ t, (compare a k).isLE = true) → α
-- Mathlib.Algebra.Group.Fin.Tuple
Matrix.add_cons : ∀ {α : Type u_1} {n : ℕ} [inst : Add α] (v : Fin n.succ → α) (y : α) (w : Fin n → α),
  v + Matrix.vecCons y w = Matrix.vecCons (Matrix.vecHead v + y) (Matrix.vecTail v + w)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Equivalence.mapAddMon.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [inst_6 : e.IsMonoidal],
  e.mapAddMon =
    { functor := e.functor.mapAddMon, inverse := e.inverse.mapAddMon,
      unitIso :=
        CategoryTheory.Functor.mapAddMonIdIso.symm ≪≫
          CategoryTheory.Functor.mapAddMonNatIso e.unitIso ≪≫ CategoryTheory.Functor.mapAddMonCompIso,
      counitIso :=
        CategoryTheory.Functor.mapAddMonCompIso.symm ≪≫
          CategoryTheory.Functor.mapAddMonNatIso e.counitIso ≪≫ CategoryTheory.Functor.mapAddMonIdIso,
      functor_unitIso_comp := ⋯ }
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.UnitaryGroup.coeFun : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      {α : Type v} →
        [inst_2 : CommRing α] → [inst_3 : StarRing α] → CoeFun ↥(Matrix.unitaryGroup n α) fun x => n → n → α
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
/-- If every finite set of algebraically independent element has cardinality at most `n`,
then the same is true for arbitrary sets of algebraically independent elements.  -/
algebraicIndependent_bounded_of_finset_algebraicIndependent_bounded : ∀ {R : Type u_2} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {n : ℕ},
  (∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → s.card ≤ n) →
    ∀ (s : Set A), AlgebraicIndependent R Subtype.val → Cardinal.mk ↑s ≤ ↑n
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.one_apply : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOne M] [inst_1 : MulOneClass N] (x : M), 1 x = 1
-- Mathlib.Data.List.Map2
List.map₂Right'.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Option α → β → γ) (as : List α) (bs : List β),
  List.map₂Right' f as bs = List.map₂Left' (flip f) bs as
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.isColimitOfConeOfCoconeRightOp_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cocone F.rightOp}
  (hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfCoconeRightOp c))
  (s : CategoryTheory.Limits.Cocone F.rightOp),
  (CategoryTheory.Limits.isColimitOfConeOfCoconeRightOp F hc).desc s =
    (hc.lift (CategoryTheory.Limits.coneOfCoconeRightOp s)).op
-- Mathlib.Algebra.EuclideanDomain.Defs
EuclideanDomain.instDiv : {R : Type u} → [EuclideanDomain R] → Div R