mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Sheaves.EtaleSpace
/-- A germ at `base` (formally, an element of the stalk of `F` at `base`).  -/
TopCat.Presheaf.EtaleSpace.germ : {X : TopCat} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {CC : C → Type v} →
        {FC : C → C → Type w} →
          [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
            [inst_2 : CategoryTheory.ConcreteCategory C FC] →
              [inst_3 : CategoryTheory.Limits.HasColimits C] →
                {F : TopCat.Presheaf C X} → (self : F.EtaleSpace) → CategoryTheory.ToType (F.stalk self.base)
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
CategoryTheory.Abelian.pseudoEqual_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : C}, Std.Symm (CategoryTheory.Abelian.PseudoEqual P)
-- Mathlib.Order.Interval.Finset.Defs
/-- `Finset.uIcc a b` is the set of elements lying between `a` and `b`, with `a` and `b` included.
Note that we define it more generally in a lattice as `Finset.Icc (a ⊓ b) (a ⊔ b)`. In a
product type, `Finset.uIcc` corresponds to the bounding box of the two elements.  -/
FinsetInterval.«term[[_,_]]» : Lean.ParserDescr
-- Mathlib.Geometry.Manifold.Notation
/-- Finds the most recent local declaration for which `p fvar type` produces `some a`.
Skips implementation details; instantiates mvars in and runs `whnfR` on `type` before providing it
to `p`.  -/
_private.Mathlib.Geometry.Manifold.Notation.0.Manifold.Elab.findSomeLocalHyp? : {α : Type} → (Lean.Expr → Lean.Expr → Lean.MetaM (Option α)) → Lean.MetaM (Option α)
-- Init.Data.Int.Lemmas
Int.neg_mul_eq_mul_neg : ∀ (a b : ℤ), -(a * b) = a * -b
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.map_map_equiv : ∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type w'} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β}
  {f : α → β → γ} {g : α → γ → δ},
  m.WF → (Std.HashMap.Raw.map g (Std.HashMap.Raw.map f m)).Equiv (Std.HashMap.Raw.map (fun k v => g k (f k v)) m)
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.takeWhile₂TR.go.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List β → List α → List β → Sort u_3) (x : List α) (x_1 : List β)
  (acca : List α) (accb : List β)
  (h_1 :
    (a : α) →
      (as : List α) →
        (b : β) → (bs : List β) → (acca : List α) → (accb : List β) → motive (a :: as) (b :: bs) acca accb)
  (h_2 : (x : List α) → (x_2 : List β) → (acca : List α) → (accb : List β) → motive x x_2 acca accb),
  (∀ (a : α) (as : List α) (b : β) (bs : List β), x = a :: as → x_1 = b :: bs → False) →
    (match x, x_1, acca, accb with
      | a :: as, b :: bs, acca, accb => h_1 a as b bs acca accb
      | x, x_3, acca, accb => h_2 x x_3 acca accb) =
      h_2 x x_1 acca accb
-- Lean.Elab.Match
Lean.Elab.Term.GeneralizeResult.mk : Array Lean.Elab.Term.Discr →
  Array Lean.FVarId → Lean.Expr → Array Lean.Elab.Term.TermMatchAltView → Bool → Lean.Elab.Term.GeneralizeResult
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.instHasPullbackHomDiscretePUnitOfHasPullbacksAlong : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T) {X Y : T}
  (f : X ⟶ Y) [P.HasPullbacksAlong f] (A : P.Over Q Y), CategoryTheory.Limits.HasPullback A.hom f
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.convexCombPair_restrict_restrict_compl : ∀ {I : Type u_6} {K : Type u_8} [inst : Semifield K] [inst_1 : LinearOrder K] [inst_2 : IsStrictOrderedRing K]
  (w : Convexity.StdSimplex K I) (s : Set I) (hs : ∃ x ∈ s, w.weights x ≠ 0) (hs' : ∃ x ∈ sᶜ, w.weights x ≠ 0)
  [inst_3 : DecidablePred fun x => x ∈ s],
  Convexity.convexCombPair ((Finsupp.filter (fun x => x ∈ s) w.weights).sum fun _x k => k)
      ((Finsupp.filter (fun x => x ∉ s) w.weights).sum fun _x k => k) ⋯ ⋯ ⋯ (w.restrict s hs) (w.restrict sᶜ hs') =
    w
-- Init.Control.Lawful.MonadLift.Basic
/-- Lifting preserves `bind`  -/
LawfulMonadLiftT.monadLift_bind : ∀ {m : Type u → Type v} {n : Type u → Type w} {inst : Monad m} {inst_1 : Monad n} {inst_2 : MonadLiftT m n}
  [self : LawfulMonadLiftT m n] {α β : Type u} (ma : m α) (f : α → m β),
  monadLift (ma >>= f) = do
    let x ← monadLift ma
    monadLift (f x)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- `Contravariant` is useful to formulate succinctly statements about the interactions between an
action of a Type on another one and a relation on the acted-upon Type.

See the `ContravariantClass` doc-string for its meaning.  -/
Contravariant : (M : Type u_1) → (N : Type u_2) → (M → N → N) → (N → N → Prop) → Prop
-- Mathlib.Algebra.Group.Submonoid.BigOperators
Submonoid.coe_multiset_prod : ∀ {M : Type u_4} [inst : CommMonoid M] (S : Submonoid M) (m : Multiset ↥S), ↑m.prod = (Multiset.map Subtype.val m).prod
-- Mathlib.RingTheory.Unramified.Basic
Algebra.FormallyUnramified.lift_unique_of_ringHom : ∀ {R : Type v} [inst : CommRing R] {A : Type u} [inst_1 : CommRing A] [inst_2 : Algebra R A] {B : Type w}
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [Algebra.FormallyUnramified R A] {C : Type u_1} [inst_6 : Ring C]
  (f : B →+* C), IsNilpotent (RingHom.ker f) → ∀ (g₁ g₂ : A →ₐ[R] B), f.comp ↑g₁ = f.comp ↑g₂ → g₁ = g₂
-- Mathlib.Algebra.Symmetrized
SymAlg.unsym_inv : ∀ {α : Type u_1} [inst : Inv α] (a : αˢʸᵐ), SymAlg.unsym a⁻¹ = (SymAlg.unsym a)⁻¹
-- Mathlib.RepresentationTheory.Intertwining
Representation.TensorProduct.toLinearMap_assoc : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : CommSemiring 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), (↑(Representation.TensorProduct.assoc ρ σ τ)).toLinearMap = ↑(TensorProduct.assoc A V W U)
-- Mathlib.Data.Stream.Init
Stream'.map.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Stream' α) (n : ℕ), Stream'.map f s n = f (s.get n)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Complex.contDiff_cos : ∀ {n : WithTop ℕ∞}, ContDiff ℂ n Complex.cos
-- Mathlib.Algebra.Category.AlgCat.Limits
AlgCat.instAlgebraElemForallObjCompForgetAlgHomCarrierSections : {R : Type u} →
  [inst : CommRing R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.Category.{t, v} J] →
        (F : CategoryTheory.Functor J (AlgCat R)) → Algebra R ↑(F.comp (CategoryTheory.forget (AlgCat R))).sections
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
OpenPartialHomeomorph.MDifferentiable.mdifferentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {e : OpenPartialHomeomorph M M'},
  OpenPartialHomeomorph.MDifferentiable I I' e → ∀ {x : M}, x ∈ e.source → MDiffAt ↑e x
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticWith.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (range : Lean.Lsp.Range) (fullRange? : Option Lean.Lsp.Range)
  (severity? : Option Lean.Lsp.DiagnosticSeverity) (isSilent? : Option Bool) (code? : Option Lean.Lsp.DiagnosticCode)
  (source? : Option String) (message : α) (tags? : Option (Array Lean.Lsp.DiagnosticTag))
  (leanTags? : Option (Array Lean.Lsp.LeanDiagnosticTag))
  (relatedInformation? : Option (Array Lean.Lsp.DiagnosticRelatedInformation)) (data? : Option Lean.Json),
  sizeOf
      { range := range, fullRange? := fullRange?, severity? := severity?, isSilent? := isSilent?, code? := code?,
        source? := source?, message := message, tags? := tags?, leanTags? := leanTags?,
        relatedInformation? := relatedInformation?, data? := data? } =
    1 + sizeOf range + sizeOf fullRange? + sizeOf severity? + sizeOf isSilent? + sizeOf code? + sizeOf source? +
              sizeOf message +
            sizeOf tags? +
          sizeOf leanTags? +
        sizeOf relatedInformation? +
      sizeOf data?
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RooSliceData.mk.inj : ∀ {α : Type u} {β : α → Type v} {inst : Ord α} {treeMap : Std.DTreeMap.Internal.Impl α β} {range : Std.Roo α}
  {treeMap_1 : Std.DTreeMap.Internal.Impl α β} {range_1 : Std.Roo α},
  { treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 } →
    treeMap = treeMap_1 ∧ range = range_1
-- Mathlib.Geometry.Euclidean.PerpBisector
Isometry.preimage_perpBisector : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {V' : Type u_3} {P' : Type u_4} [inst_4 : NormedAddCommGroup V']
  [inst_5 : InnerProductSpace ℝ V'] [inst_6 : MetricSpace P'] [inst_7 : NormedAddTorsor V' P'] {f : P → P'},
  Isometry f → ∀ (p₁ p₂ : P), f ⁻¹' ↑(AffineSubspace.perpBisector (f p₁) (f p₂)) = ↑(AffineSubspace.perpBisector p₁ p₂)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.coe_coe'' : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), ⇑↑↑e = ⇑e
-- Mathlib.Topology.DiscreteSubset
tendsto_cofinite_cocompact_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace Y] {f : X → Y},
  Filter.Tendsto f Filter.cofinite (Filter.cocompact Y) ↔ ∀ (K : Set Y), IsCompact K → (f ⁻¹' K).Finite
-- Mathlib.Algebra.Group.Defs
neg_eq_zero_sub : ∀ {G : Type u_1} [inst : SubNegMonoid G] (x : G), -x = 0 - x
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
Real.hasDerivAt_log : ∀ {x : ℝ}, x ≠ 0 → HasDerivAt Real.log x⁻¹ x
-- Lean.Elab.PreDefinition.Main
_private.Lean.Elab.PreDefinition.Main.0.Lean.Elab.partitionPreDefs : Array Lean.Elab.PreDefinition → Array (Array Lean.Elab.PreDefinition)
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.compl_mem : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L : BooleanSubalgebra α} {a : α}, a ∈ L → aᶜ ∈ L
-- Mathlib.Order.Monotone.Defs
Antitone.comp_monotoneOn : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β} {s : Set α}, Antitone g → MonotoneOn f s → AntitoneOn (g ∘ f) s
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {f : α → Bool} {k : α},
  (Std.ExtTreeSet.filter f t).get? k = Option.filter f (t.get? k)
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.ΓSpec.adjunction_homEquiv_apply : ∀ {X : AlgebraicGeometry.Scheme} {R : CommRingCatᵒᵖ}
  (f : Opposite.op (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op X)) ⟶ R),
  (AlgebraicGeometry.ΓSpec.adjunction.homEquiv X R) f =
    { toLRSHom' := (AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.homEquiv X.toLocallyRingedSpace R) f }
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preBeth_succ : ∀ (o : Ordinal.{u_1}), Cardinal.preBeth (Order.succ o) = 2 ^ Cardinal.preBeth o
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.eq_symm_apply : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] {m : M} {n : N} (e : M ≃ₗ⁅R,L⁆ N), m = e.symm n ↔ e m = n
-- Std.Http.Data.Headers.Basic
Std.Http.Header.TransferEncoding.mk.injEq : ∀ (codings : Array String) (isValid : Std.Http.Header.TransferEncoding.Validate codings = true)
  (codings_1 : Array String) (isValid_1 : Std.Http.Header.TransferEncoding.Validate codings_1 = true),
  ({ codings := codings, isValid := isValid } = { codings := codings_1, isValid := isValid_1 }) = (codings = codings_1)
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.div_lt_floor : ∀ {x : ℝ}, 2 / (1 - 2 / Real.exp 1) ≤ x → x / Real.exp 1 < ↑⌊x / 2⌋₊
-- Init.Data.Int.Lemmas
_private.Init.Data.Int.Lemmas.0.Int.add_assoc.aux2 : ∀ (m n k : ℕ), Int.negSucc m + Int.negSucc n + ↑k = Int.negSucc m + (Int.negSucc n + ↑k)
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
CovariantDerivative.mk.injEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)]
  [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] [inst_14 : FiberBundle F V]
  (toFun : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x)
  (isCovariantDerivativeOnUniv : IsCovariantDerivativeOn F toFun)
  (toFun_1 : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x)
  (isCovariantDerivativeOnUniv_1 : IsCovariantDerivativeOn F toFun_1),
  ({ toFun := toFun, isCovariantDerivativeOnUniv := isCovariantDerivativeOnUniv } =
      { toFun := toFun_1, isCovariantDerivativeOnUniv := isCovariantDerivativeOnUniv_1 }) =
    (toFun = toFun_1)
-- Mathlib.LinearAlgebra.Dimension.Localization
IsBaseChange.finrank_eq_of_le_nonZeroDivisors : ∀ {R : Type uR} (S : Type uS) {M : Type uM} {N : Type uN} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Algebra R S]
  [inst_7 : Module S N] [IsScalarTower R S N] {p : Submonoid R} [IsLocalization p S] (f : M →ₗ[R] N)
  [IsLocalizedModule p f],
  p ≤ nonZeroDivisors R →
    ∀ [Module.Free S N] [StrongRankCondition S] {T : Type uT} [inst_13 : CommRing T] [inst_14 : Algebra R T],
      Algebra.algebraMapSubmonoid T p ≤ nonZeroDivisors T →
        ∀ [StrongRankCondition (TensorProduct R S T)] {P : Type uP} [inst_16 : AddCommGroup P] [inst_17 : Module R P]
          [inst_18 : Module T P] [inst_19 : IsScalarTower R T P] {g : M →ₗ[R] P},
          IsBaseChange T g → Module.finrank T P = Module.finrank R M
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionObj : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction Cᵒᵖ Dᵒᵖ] (c : C) (d : D),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d =
    Opposite.unop (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj (Opposite.op c) (Opposite.op d))
-- Mathlib.NumberTheory.Height.MvPolynomial
/-- Let `A : ι' × ι → K`, which we can interpret as a linear map from `ι → K` to `ι' → K`.
Let `x : ι → K` be a tuple. Then the logarithmic height of `A x` is bounded by
`totalWeight K * log #ι + logHeight A + logHeight x`.

(Note that here we do not need to assume that `ι` is nonempty, due to the convenient
junk value `log 0 = 0`.)  -/
Height.logHeight_linearMap_apply_le : ∀ {K : Type u_1} [inst : Field K] {ι : Type u_2} {ι' : Type u_3} [inst_1 : Fintype ι] [Finite ι']
  [inst_3 : Height.AdmissibleAbsValues K] (A : ι' × ι → K) (x : ι → K),
  (Height.logHeight fun j => ∑ i, A (j, i) * x i) ≤
    ↑(Height.totalWeight K) * Real.log ↑(Nat.card ι) + Height.logHeight A + Height.logHeight x
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.of_injective : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst_1 : DecidableEq ι] (i : ι),
  Function.Injective ⇑(DirectSum.of β i)
-- Mathlib.Data.Set.Image
Set.range_comp_subset_range : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → γ), Set.range (g ∘ f) ⊆ Set.range g
-- Mathlib.Data.Finsupp.Single
Finsupp.support_erase : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] [inst_1 : DecidableEq α] {a : α} {f : α →₀ M},
  (Finsupp.erase a f).support = f.support.erase a
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.mk.injEq : ∀ {α : Type u_4} [inst : TopologicalSpace α] (carrier : Set α) (isCompact' : IsCompact carrier) (carrier_1 : Set α)
  (isCompact'_1 : IsCompact carrier_1),
  ({ carrier := carrier, isCompact' := isCompact' } = { carrier := carrier_1, isCompact' := isCompact'_1 }) =
    (carrier = carrier_1)
-- Std.Sat.CNF.Basic
Std.Sat.CNF.add.eq_1 : ∀ {α : Type u_1} (c : Std.Sat.CNF.Clause α) (f : Std.Sat.CNF α), Std.Sat.CNF.add c f = { clauses := f.clauses.push c }
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.ω₂_mem_lattice : ∀ (L : PeriodPair), L.ω₂ ∈ L.lattice
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.ext : ∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {x y : C ≌ D},
  x.functor = y.functor → x.inverse = y.inverse → x.unitIso ≍ y.unitIso → x.counitIso ≍ y.counitIso → x = y
-- Aesop.Util.UnorderedArraySet
/-- O(n)  -/
Aesop.UnorderedArraySet.any : {α : Type u_1} → [inst : BEq α] → (α → Bool) → (s : Aesop.UnorderedArraySet α) → optParam ℕ 0 → optParam ℕ s.size → Bool
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.linearMapAt_symm : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : AddCommMonoid F]
  [inst_5 : Module R F] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_8 : Bundle.Trivialization.IsLinear R e] {b : B},
  b ∈ e.baseSet → ∀ (y : F), (Bundle.Trivialization.linearMapAt R e b) (e.symm b y) = y
-- Mathlib.Algebra.Group.Action.Faithful
/-- `instSMulOfMul` is faithful when there is a (right) identity.  -/
instFaithfulSMul : ∀ (R : Type u_4) [inst : MulOneClass R], FaithfulSMul R R
-- Mathlib.Topology.Inseparable
stableUnderGeneralization_univ : ∀ {X : Type u_1} [inst : TopologicalSpace X], StableUnderGeneralization Set.univ
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
CategoryTheory.Limits.HasStrictTerminalObjects.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (∀ {I A : C} (f : I ⟶ A) (a : CategoryTheory.Limits.IsTerminal I), CategoryTheory.IsIso f) →
    CategoryTheory.Limits.HasStrictTerminalObjects C
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.LaxTrans.Modification.mk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} →
          {η θ : F ⟶ G} →
            (app : (a : B) → η.app a ⟶ θ.app a) →
              autoParam
                  (∀ {a b : B} (f : a ⟶ b),
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f))
                        (θ.naturality f) =
                      CategoryTheory.CategoryStruct.comp (η.naturality f)
                        (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b)))
                  CategoryTheory.Lax.LaxTrans.Modification.naturality._autoParam →
                CategoryTheory.Lax.LaxTrans.Modification η θ
-- Mathlib.Analysis.Fourier.Notation
FourierInvModule.mk : {R : Type u_5} →
  {E : Type u_6} →
    {F : outParam (Type u_7)} →
      [inst : Add E] →
        [inst_1 : Add F] →
          [inst_2 : SMul R E] →
            [inst_3 : SMul R F] →
              (toFourierTransformInv : FourierTransformInv E F) →
                (∀ (f g : E),
                    FourierTransformInv.fourierInv (f + g) =
                      FourierTransformInv.fourierInv f + FourierTransformInv.fourierInv g) →
                  (∀ (r : R) (f : E), FourierTransformInv.fourierInv (r • f) = r • FourierTransformInv.fourierInv f) →
                    FourierInvModule R E F
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.Result'.isNat.inj : ∀ {inst lit proof inst_1 lit_1 proof_1 : Lean.Expr},
  Mathlib.Meta.NormNum.Result'.isNat inst lit proof = Mathlib.Meta.NormNum.Result'.isNat inst_1 lit_1 proof_1 →
    inst = inst_1 ∧ lit = lit_1 ∧ proof = proof_1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get_eq_getD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {a : α} {fallback : β a} {h' : a ∈ t}, t.get a h' = t.getD a fallback
-- Std.Sat.AIG.CNF
/-- The CNF cache. It keeps track of AIG nodes that we already turned into CNF to avoid adding the same
CNF twice.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.Cache : Std.Sat.AIG ℕ → Std.Sat.CNF ℕ → Type
-- Mathlib.CategoryTheory.Whiskering
/-- The "postcomposition" with a functor `E ⥤ E'` gives a functor
`(E ⥤ E') ⥤ (C₁ ⥤ C₂ ⥤ E) ⥤ C₁ ⥤ C₂ ⥤ E'`.  -/
CategoryTheory.Functor.postcompose₂ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {E : Type u_7} →
          [inst_2 : CategoryTheory.Category.{v_7, u_7} E] →
            {E' : Type u_8} →
              [inst_3 : CategoryTheory.Category.{v_8, u_8} E'] →
                CategoryTheory.Functor (CategoryTheory.Functor E E')
                  (CategoryTheory.Functor (CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E))
                    (CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E')))
-- Init.Data.List.Lemmas
List.getElem_reverse : ∀ {α : Type u_1} {l : List α} {i : ℕ} (h : i < l.reverse.length), l.reverse[i] = l[l.length - 1 - i]
-- Mathlib.Topology.Instances.EReal.Lemmas
/-- The multiplication on `EReal` is continuous except at indeterminacies
(i.e. whenever one value is zero and the other infinite).  -/
EReal.continuousAt_mul : ∀ {p : EReal × EReal},
  p.1 ≠ 0 ∨ p.2 ≠ ⊥ → p.1 ≠ 0 ∨ p.2 ≠ ⊤ → p.1 ≠ ⊥ ∨ p.2 ≠ 0 → p.1 ≠ ⊤ ∨ p.2 ≠ 0 → ContinuousAt (fun p => p.1 * p.2) p
-- Mathlib.Order.WellFounded
WellFounded.wellFoundedLT_iff_exists_minimal : ∀ {α : Type u_1} [inst : Preorder α], WellFoundedLT α ↔ ∀ (s : Set α), s.Nonempty → ∃ m, Minimal (fun x => x ∈ s) m