mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.DirectSum.Basic
/-- The natural map between `⨁ i (j : α i), δ i j` and `Π₀ (i : Σ i, α i), δ i.1 i.2`, inverse of
`curry`.  -/
DirectSum.sigmaUncurry : {ι : Type v} →
  [DecidableEq ι] →
    {α : ι → Type u} →
      {δ : (i : ι) → α i → Type w} →
        [inst : (i : ι) → (j : α i) → AddCommMonoid (δ i j)] →
          (DirectSum ι fun i => DirectSum (α i) fun j => δ i j) →+ DirectSum ((_i : ι) × α _i) fun i => δ i.fst i.snd
-- Mathlib.Combinatorics.Matroid.Minor.Order
/-- `<m` denotes the strict minor relation on matroids.  -/
Matroid.«term_<m_» : Lean.TrailingParserDescr
-- Lean.Data.Lsp.Internal
/-- Selection range of this parent decl.  -/
Lean.Lsp.DeclInfo.selectionRange : Lean.Lsp.DeclInfo → Lean.Lsp.Range
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
/-- `Set.powersetCard α n` as a `SubAddAction` of `Finsetα`. -/
Set.powersetCard.subAddAction : (G : Type u_1) →
  [inst : AddGroup G] →
    (α : Type u_2) → [inst_1 : AddAction G α] → ℕ → [inst_2 : DecidableEq α] → SubAddAction G (Finset α)
-- Init.Data.SInt.Bitwise
UInt64.toInt64_or : ∀ (a b : UInt64), (a ||| b).toInt64 = a.toInt64 ||| b.toInt64
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.instDecidableEqIterator.decEq.match_1.eq_1 : ∀ (motive : String.Legacy.Iterator → String.Legacy.Iterator → Sort u_1) (a : String) (a_1 : String.Pos.Raw) (b : String)
  (b_1 : String.Pos.Raw)
  (h_1 :
    (a : String) →
      (a_2 : String.Pos.Raw) →
        (b : String) → (b_2 : String.Pos.Raw) → motive { s := a, i := a_2 } { s := b, i := b_2 }),
  (match { s := a, i := a_1 }, { s := b, i := b_1 } with
    | { s := a, i := a_2 }, { s := b, i := b_2 } => h_1 a a_2 b b_2) =
    h_1 a a_1 b b_1
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.LiftableCone.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C}
  {F : CategoryTheory.Functor C D} {c : CategoryTheory.Limits.Cone (K.comp F)}
  (liftedCone : CategoryTheory.Limits.Cone K) (validLift : F.mapCone liftedCone ≅ c)
  (liftedCone_1 : CategoryTheory.Limits.Cone K) (validLift_1 : F.mapCone liftedCone_1 ≅ c),
  ({ liftedCone := liftedCone, validLift := validLift } = { liftedCone := liftedCone_1, validLift := validLift_1 }) =
    (liftedCone = liftedCone_1 ∧ validLift ≍ validLift_1)
-- Lean.DocString.Types
/-- Inline content that is part of the text flow.
 -/
Lean.Doc.Inline : Type u → Type u
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.mk.injEq : ∀ {R : Type u} {a b : R} (re im re_1 im_1 : R),
  ({ re := re, im := im } = { re := re_1, im := im_1 }) = (re = re_1 ∧ im = im_1)
-- Std.Http.Protocol.H1.Writer
Std.Http.Protocol.H1.Writer.State.pending.sizeOf_spec : sizeOf Std.Http.Protocol.H1.Writer.State.pending = 1
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
/-- The `edges` of a walk is the list of edges it visits in order.
This is defined to be the list of edges underlying `SimpleGraph.Walk.darts`.  -/
SimpleGraph.Walk.edges : {V : Type u} → {G : SimpleGraph V} → {u v : V} → G.Walk u v → List (Sym2 V)
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.tendsto_zero_sumCoeffsExp : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r), Filter.Tendsto (fun p => ∑ i, a i * b i ^ p) Filter.atTop (nhds 0)
-- Mathlib.Tactic.Relation.Symm
/-- If `e` is the form `@R .. x y`, where `R` is a symmetric
relation, return `some (R, x, y)`.
As a special case, if `e` is `@HEq α a β b`, return ``some (`HEq, a, b)``.  -/
Lean.Expr.relSidesIfSymm? : Lean.Expr → Lean.MetaM (Option (Lean.Name × Lean.Expr × Lean.Expr))
-- Mathlib.RepresentationTheory.Rep.Basic
_private.Mathlib.RepresentationTheory.Rep.Basic.0.Rep.mk.inj : ∀ {k : Type u} {G : Type v} {inst : Semiring k} {inst_1 : Monoid G} {V : Type w} {hV1 : AddCommGroup V}
  {hV2 : Module k V} {ρ : Representation k G V} {V_1 : Type w} {hV1_1 : AddCommGroup V_1} {hV2_1 : Module k V_1}
  {ρ_1 : Representation k G V_1},
  { V := V, hV1 := hV1, hV2 := hV2, ρ := ρ } = { V := V_1, hV1 := hV1_1, hV2 := hV2_1, ρ := ρ_1 } →
    V = V_1 ∧ hV1 ≍ hV1_1 ∧ hV2 ≍ hV2_1 ∧ ρ ≍ ρ_1
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoidHom.compr₂.eq_1 : ∀ {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddCommMonoid P] [inst_3 : AddCommMonoid Q] (f : M →+ N →+ P) (g : P →+ Q),
  f.compr₂ g = (AddMonoidHom.compHom g).comp f
-- Init.Data.SInt.Bitwise
Int64.toInt16_and : ∀ (a b : Int64), (a &&& b).toInt16 = a.toInt16 &&& b.toInt16
-- Mathlib.Data.EReal.Operations
EReal.neg_bot : -⊥ = ⊤
-- Mathlib.Data.Finsupp.Antidiagonal
Finsupp.image_sumElim_product_antidiagonal : ∀ {α : Type u} [inst : DecidableEq α] {β : Type u_1} [inst_1 : DecidableEq β] {x : α →₀ ℕ} {y : β →₀ ℕ},
  Finset.image
      (fun x =>
        match x with
        | ((x, y), z, w) => (x.sumElim z, y.sumElim w))
      (Finset.HasAntidiagonal.antidiagonal x ×ˢ Finset.HasAntidiagonal.antidiagonal y) =
    Finset.HasAntidiagonal.antidiagonal (x.sumElim y)
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
/-- A type synonym for matroids with the isRestriction order.
(The `PartialOrder` on `Matroid α` is reserved for the minor order)  -/
Matroid.Matroidᵣ : Type u_2 → Type u_2
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.comp_apply : ∀ {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) (r : ↑R),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) r =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) r)
-- Mathlib.Analysis.Normed.Order.Lattice
HasSolidNorm.continuousSup : ∀ {α : Type u_2} [inst : NormedAddCommGroup α] [inst_1 : Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α],
  ContinuousSup α
-- Lean.Data.Lsp.TextSync
Lean.Lsp.SaveOptions : Type
-- Lean.Data.AssocList
Lean.AssocList.insertNew : {α : Type u} → {β : Type v} → Lean.AssocList α β → α → β → Lean.AssocList α β
-- Mathlib.Algebra.Group.Units.Defs
Units.mul_inv : ∀ {α : Type u} [inst : Monoid α] (a : αˣ), ↑a * ↑a⁻¹ = 1
-- Mathlib.Analysis.Normed.Module.RieszLemma
/-- A version of Riesz lemma: given a strict closed subspace `F`, one may find an element of norm `≤ R`
which is at distance at least `1` of every element of `F`. Here, `R` is any given constant
strictly larger than the norm of an element of norm `> 1`. For a version without an `R`, see
`riesz_lemma`, and for a variant giving an element with norm
exactly one assuming stronger assumptions on the underlying field, see
`riesz_lemma_of_lt_one`.

Since we are considering a general nontrivially normed field, there may be a gap in possible norms
(for instance no element of norm in `(1,2)`). Hence, we cannot allow `R` arbitrarily close to `1`,
and require `R > ‖c‖` for some `c : 𝕜` with norm `> 1`.
 -/
riesz_lemma_of_norm_lt : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {c : 𝕜},
  1 < ‖c‖ →
    ∀ {R : ℝ}, ‖c‖ < R → ∀ {F : Subspace 𝕜 E}, IsClosed ↑F → (∃ x, x ∉ F) → ∃ x₀, ‖x₀‖ ≤ R ∧ ∀ y ∈ F, 1 ≤ ‖x₀ - y‖
-- Lean.Meta.Tactic.Intro
/-- Given a goal `... |- β → α`, returns a goal `... ⊢ α`.
Like `intro h; clear h`, but without ever appending to the local context.
 -/
Lean.MVarId.intro1_ : Lean.MVarId → Lean.MetaM Lean.MVarId
-- Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
_private.Mathlib.Analysis.SpecificLimits.ArithmeticGeometric.0.arithGeom.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- An induction (and recursion) principle for proving results about all submodules of a fixed
finite free module `M`. A property is true for all submodules of `M` if it satisfies the following
"inductive step": the property is true for a submodule `N` if it's true for all submodules `N'`
of `N` with the property that there exists `0 ≠ x ∈ N` such that the sum `N' + Rx` is direct.  -/
Submodule.inductionOnRank : {ι : Type w} →
  {R : Type u_3} →
    {M : Type u_4} →
      [inst : Ring R] →
        [StrongRankCondition R] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] →
              [IsDomain R] →
                [Finite ι] →
                  Module.Basis ι R M →
                    (P : Submodule R M → Sort u_2) →
                      ((N : Submodule R M) →
                          ((N' : Submodule R M) →
                              N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') →
                            P N) →
                        (N : Submodule R M) → P N
-- Lean.Meta.Tactic.Simp.Types
/-- If `cache := true` the result is cached.
Warning: we will remove this field in the future. It is currently used by
`arith := true`, but we can now refactor the code to avoid the hack.
 -/
Lean.Meta.Simp.Result.cache : Lean.Meta.Simp.Result → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPushout.isIso_inr_of_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P},
  CategoryTheory.IsPushout f g inl inr →
    autoParam (CategoryTheory.IsIso f) CategoryTheory.IsPushout.isIso_inr_of_isIso._auto_1 → CategoryTheory.IsIso inr
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.toCycles_cyclesMap : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j')
  (g' : j' ⟶ k') (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (fg' : i' ⟶ k')
  (h' : CategoryTheory.CategoryStruct.comp f' g' = fg')
  (α : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g')
  (β : CategoryTheory.ComposableArrows.mk₁ fg ⟶ CategoryTheory.ComposableArrows.mk₁ fg') (n : ℤ),
  autoParam (β.app 0 = α.app 0) CategoryTheory.Abelian.SpectralObject.toCycles_cyclesMap._auto_1 →
    autoParam (β.app 1 = α.app 2) CategoryTheory.Abelian.SpectralObject.toCycles_cyclesMap._auto_3 →
      CategoryTheory.CategoryStruct.comp (X.toCycles f g fg h n) (X.cyclesMap f g f' g' α n) =
        CategoryTheory.CategoryStruct.comp ((X.H n).map β) (X.toCycles f' g' fg' h' n)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.reverseEquiv_apply : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (x : CliffordAlgebra Q), CliffordAlgebra.reverseEquiv x = CliffordAlgebra.reverse x
-- Mathlib.RingTheory.Ideal.Quotient.Over
Ideal.ncard_primesOver_quotient_singleton_lt_of_notMem : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (P : Ideal R) (e : S)
  (P' : Ideal S) [P'.IsPrime] [P'.LiesOver P],
  e ∉ P' → (P.primesOver S).Finite → (P.primesOver (S ⧸ Ideal.span {e})).ncard < (P.primesOver S).ncard
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.dvd_term_of_dvd_eval_of_dvd_terms : ∀ {S : Type v} [inst : CommRing S] {z p : S} {f : Polynomial S} (i : ℕ),
  p ∣ Polynomial.eval z f → (∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j) → p ∣ f.coeff i * z ^ i
-- Mathlib.Topology.EMetricSpace.Weak
instEDistWithTop.eq_1 : ∀ {α : Type u} [inst : EDist α],
  instEDistWithTop =
    {
      edist := fun x x_1 =>
        match x, x_1 with
        | none, some x => ⊤
        | none, none => 0
        | some x, none => ⊤
        | some x, some y => edist x y }
-- Lean.Elab.ParseImportsFast
_private.Lean.Elab.ParseImportsFast.0.Lean.ParseImports.keywordCore.go : String →
  Lean.ParseImports.Parser →
    Lean.ParseImports.Parser →
      String → Lean.ParseImports.State → String.Pos.Raw → String.Pos.Raw → Lean.ParseImports.State
-- Lean.LocalContext
/-- A LocalContext is an ordered set of local variable declarations.
It is used to store the free variables (also known as local constants) that
are in scope. It also maps free variables corresponding to auxiliary declarations
(recursive references and `where` and `let rec` bindings) to their fully-qualified global names.

When inspecting a goal or expected type in the infoview, the local
context is all of the variables above the `⊢` symbol.
  -/
Lean.LocalContext : Type
-- Init.Prelude
/-- Converts a `List α` into an `Array α`.

The function `List.toArray` is preferred.

At runtime, this constructor is overridden by `List.toArrayImpl` and is `O(n)` in the length of
the list.
 -/
Array.mk : {α : Type u} → List α → Array α
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
/-- The property of preserving products expressed in terms of binary fans.  -/
CategoryTheory.Limits.mapIsLimitOfPreservesOfIsLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {P X Y : C} →
            (f : P ⟶ X) →
              (g : P ⟶ Y) →
                [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X Y) G] →
                  CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk f g) →
                    CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk (G.map f) (G.map g))
-- Std.Http.Protocol.H1.Message
Std.Http.Protocol.H1.Direction.noConfusionType : Sort v✝ → Std.Http.Protocol.H1.Direction → Std.Http.Protocol.H1.Direction → Sort v✝
-- Mathlib.Algebra.Star.Pi
Pi.instStarMulForall : {I : Type u} → {f : I → Type v} → [inst : (i : I) → Mul (f i)] → [(i : I) → StarMul (f i)] → StarMul ((i : I) → f i)
-- Lean.Data.JsonRpc
/-- A Response Message sent as a result of a request.  -/
Lean.JsonRpc.Message.response : Lean.JsonRpc.RequestID → Lean.Json → Lean.JsonRpc.Message
-- Mathlib.Data.TwoPointing
TwoPointing.nonempty_two_pointing_iff : ∀ {α : Type u_1}, Nonempty (TwoPointing α) ↔ Nontrivial α
-- Std.Data.TreeSet.Raw.Basic
/-- Internal implementation detail of the tree map  -/
Std.TreeSet.Raw.Equiv.inner : ∀ {α : Type u} {cmp : α → α → Ordering} {m₁ m₂ : Std.TreeSet.Raw α cmp}, m₁.Equiv m₂ → m₁.inner.Equiv m₂.inner
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.CommRingObjCat.Hom.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} {R₁ R₂ : CategoryTheory.CommRingObjCat C} {x y : R₁.Hom R₂},
  x.hom = y.hom → x = y
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.keys_filter_key : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {f : α → Bool},
  m.WF → (Std.DHashMap.Raw.filter (fun k x => f k) m).keys.Perm (List.filter f m.keys)
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction_unit_f : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} {adj : F ⊣ G}
  [inst_2 : ∀ (A : adj.toMonad.Algebra), CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))]
  (A : adj.toMonad.Algebra),
  ((CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction adj).unit.app A).f =
    (CategoryTheory.Monad.beckCoequalizer A).desc (CategoryTheory.Monad.MonadicityInternal.unitCofork A)
-- Mathlib.Analysis.Normed.Group.HomCompletion
NormedAddGroupHom.completion_neg : ∀ {G : Type u_1} [inst : SeminormedAddCommGroup G] {H : Type u_2} [inst_1 : SeminormedAddCommGroup H]
  (f : NormedAddGroupHom G H), (-f).completion = -f.completion
-- Std.Data.HashMap.Lemmas
Std.HashMap.forIn_eq_forIn_toList : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {δ : Type w} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : α × β → δ → m' (ForInStep δ)} {init : δ},
  forIn m init f = forIn m.toList init f
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.HasBinaryBiproduct.mk' : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C}, Nonempty (CategoryTheory.Limits.BinaryBiproductData P Q) → CategoryTheory.Limits.HasBinaryBiproduct P Q
-- Mathlib.Order.SymmDiff
symmDiff_eq_sup : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a b : α), symmDiff a b = a ⊔ b ↔ Disjoint a b
-- Init.SimpLemmas
and_iff_right_iff_imp : ∀ {a b : Prop}, (a ∧ b ↔ b) ↔ b → a
-- Mathlib.LinearAlgebra.Projection
Submodule.projection_apply_mem : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q) (x : E), (p.projection q hpq) x ∈ p
-- Lean.Parser.Do
Lean.Parser.Term.doUnless.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.String
String.reduceNe : Lean.Meta.Simp.Simproc
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivial.homeomorphProd_symm_apply_snd : ∀ (B : Type u_1) (F : Type u_2) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] (x : B × F),
  ((Bundle.Trivial.homeomorphProd B F).symm x).snd = x.2
-- Mathlib.Analysis.Calculus.Gradient.Basic
HasGradientAtFilter.hasDerivAtFilter' : ∀ {g : ℝ → ℝ} {g' u : ℝ} {L' : Filter ℝ}, HasGradientAtFilter g g' u L' → HasDerivAtFilter g g' (L' ×ˢ pure u)
-- Mathlib.MeasureTheory.Measure.Prod
/-- If `ν` is a finite measure, and `s ⊆ α × β` is measurable, then `x ↦ ν { y | (x, y) ∈ s }` is
a measurable function. `measurable_measure_prodMk_left` is strictly more general.  -/
measurable_measure_prodMk_left_finite : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {ν : MeasureTheory.Measure β}
  [MeasureTheory.IsFiniteMeasure ν] {s : Set (α × β)}, MeasurableSet s → Measurable fun x => ν (Prod.mk x ⁻¹' s)
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.compl_infty : ∀ {X : Type u_1}, {OnePoint.infty}ᶜ = Set.range OnePoint.some
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Algebra.intNorm_eq_zero : ∀ {A : Type u_1} {B : Type u_6} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : IsIntegrallyClosed A] [inst_4 : IsDomain A] [inst_5 : IsDomain B] [inst_6 : IsIntegrallyClosed B]
  [inst_7 : Algebra.IsIntegral A B] [inst_8 : Module.IsTorsionFree A B]
  [FiniteDimensional (FractionRing A) (FractionRing B)] {x : B}, (Algebra.intNorm A B) x = 0 ↔ x = 0
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
/-- The space of continuous multilinear maps on `Π(i : Fin (n+1)), E i` is canonically isomorphic to
the space of continuous linear maps from `E 0` to the space of continuous multilinear maps on
`Π(i : Fin n), E i.succ`, by separating the first variable. We register this isomorphism in
`continuousMultilinearCurryLeftEquiv 𝕜 E E₂`. The algebraic version (without topology) is given
in `multilinearCurryLeftEquiv 𝕜 E E₂`.

The direct and inverse maps are given by `f.curryLeft` and `f.uncurryLeft`. Use these
unless you need the full framework of linear isometric equivs.  -/
continuousMultilinearCurryLeftEquiv : (𝕜 : Type u) →
  {n : ℕ} →
    (Ei : Fin n.succ → Type wEi) →
      (G : Type wG) →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] →
            [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] →
              [inst_3 : NormedAddCommGroup G] →
                [inst_4 : NormedSpace 𝕜 G] → ContinuousMultilinearMap 𝕜 Ei G ≃ₗᵢ[𝕜] Ei 0 →L[𝕜] Ei i.succ [×n]→L[𝕜] G
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.Hom.w_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {X Y : CategoryTheory.StructuredArrow S T} (f : X ⟶ Y) {Z : D}
  (h : T.obj Y.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp X.hom
      (CategoryTheory.CategoryStruct.comp (T.map (CategoryTheory.StructuredArrow.Hom.right f)) h) =
    CategoryTheory.CategoryStruct.comp Y.hom h
-- Mathlib.Dynamics.PeriodicPts.Defs
/-- If `f` sends two periodic points `x` and `y` of positive periods to the same point,
then `x = y`.  -/
Function.IsPeriodicPt.eq_of_apply_eq : ∀ {α : Type u_1} {f : α → α} {x y : α} {m n : ℕ},
  Function.IsPeriodicPt f m x → Function.IsPeriodicPt f n y → 0 < m → 0 < n → f x = f y → x = y
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_diff_add_size_inter_eq_size_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF), m₂.WF → (m₁.diff m₂ ⋯).size + (m₁.inter m₂ ⋯).size = m₁.size
-- Mathlib.Data.Nat.Fib.Zeckendorf
List.IsZeckendorfRep.eq_1 : ∀ (l : List ℕ), l.IsZeckendorfRep = List.IsChain (fun a b => b + 2 ≤ a) (l ++ [0])
-- Mathlib.Topology.Homeomorph.Lemmas
/-- `X × {*}` is homeomorphic to `X`.  -/
Homeomorph.prodUnique : (X : Type u_1) → (Y : Type u_2) → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → [Unique Y] → X × Y ≃ₜ X
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
/-- If a category has all binary products and all weak equalizers, then it also has all
weak pullbacks. As usual, this is not an instance, since there may be a more direct way to
construct weak pullbacks.  -/
CategoryTheory.Limits.hasWeakPullbacks_of_hasBinaryProducts_of_hasWeakEqualizers : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasBinaryProducts C]
  [CategoryTheory.Limits.HasWeakEqualizers C], CategoryTheory.Limits.HasWeakPullbacks C
-- Mathlib.Data.Matrix.PEquiv
PEquiv.toMatrix_toPEquiv_mul : ∀ {l : Type u_2} {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : DecidableEq m]
  [inst_2 : NonAssocSemiring α] (f : l ≃ m) (M : Matrix m n α), f.toPEquiv.toMatrix * M = M.submatrix (⇑f) id
-- Mathlib.Order.Bounds.Basic
BddBelow.insert : ∀ {α : Type u_1} [inst : Preorder α] [IsCodirectedOrder α] {s : Set α} (a : α), BddBelow s → BddBelow (insert a s)
-- Mathlib.CategoryTheory.Monoidal.Transport
CategoryTheory.Monoidal.transportStruct_whiskerRight : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X₁ X₂ : D} (f : X₁ ⟶ X₂) (X : D),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight f X =
    e.functor.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight (e.inverse.map f) (e.inverse.obj X))
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given Localization maps `f : M →* N` for a Submonoid `S ⊆ M` and
`k : M →* Q` for a Submonoid `T ⊆ M`, such that `S ≤ T`, and we have
`l : M →* A`, the composition of the induced map `f.lift` for `k` with
the induced map `k.lift` for `l` is equal to the induced map `f.lift` for `l`.  -/
Submonoid.LocalizationMap.lift_comp_lift : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) {T : Submonoid M} (hST : S ≤ T) {Q : Type u_4} [inst_2 : CommMonoid Q]
  (k : T.LocalizationMap Q) {A : Type u_5} [inst_3 : CommMonoid A] {l : M →* A} (hl : ∀ (w : ↥T), IsUnit (l ↑w)),
  (k.lift hl).comp (f.lift ⋯) = f.lift ⋯
-- Mathlib.Data.Fin.Embedding
Fin.range_natAdd_castLEEmb : ∀ {n m : ℕ} (hmn : n ≤ m), Set.range ⇑(Fin.natAdd_castLEEmb hmn) = {i | m - n ≤ ↑i}
-- Init.Data.List.Perm
List.singleton_perm_singleton : ∀ {α : Type u_1} {a b : α}, [a].Perm [b] ↔ a = b
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVLogicalExpr.Sat.eq_1 : ∀ (x : Std.Tactic.BVDecide.BVLogicalExpr) (assign : Std.Tactic.BVDecide.BVExpr.Assignment),
  x.Sat assign = (Std.Tactic.BVDecide.BVLogicalExpr.eval assign x = true)