mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving
Continuous.compMeasurePreservingLp : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [BorelSpace X] [R1Space X]
  [inst_4 : TopologicalSpace Y] [inst_5 : MeasurableSpace Y] [BorelSpace Y] [R1Space Y] {μ : MeasureTheory.Measure X}
  {ν : MeasureTheory.Measure Y} [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure ν] {E : Type u_3}
  [inst_10 : NormedAddCommGroup E] {p : ENNReal} [inst_11 : Fact (1 ≤ p)] {Z : Type u_4} [inst_12 : TopologicalSpace Z]
  {f : Z → ↥(MeasureTheory.Lp E p ν)} {g : Z → C(X, Y)},
  Continuous f →
    Continuous g →
      ∀ (hgm : ∀ (z : Z), MeasureTheory.MeasurePreserving (⇑(g z)) μ ν),
        p ≠ ⊤ → Continuous fun z => (MeasureTheory.Lp.compMeasurePreserving ⇑(g z) ⋯) (f z)
-- Mathlib.Tactic.DepRewrite
/-- Which occurrences to rewrite.  -/
Mathlib.Tactic.DepRewrite.Config.occs : Mathlib.Tactic.DepRewrite.Config → Lean.Meta.Occurrences
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.CondIndep.condIndepSets : ∀ {Ω : Type u_1} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω}
  [inst_1 : MeasureTheory.IsFiniteMeasure μ] {s1 s2 : Set (Set Ω)},
  ProbabilityTheory.CondIndep m' (MeasurableSpace.generateFrom s1) (MeasurableSpace.generateFrom s2) hm' μ →
    ProbabilityTheory.CondIndepSets m' hm' s1 s2 μ
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.sub' : ∀ {G : Type u_2} {α : Type u_3} {β : Type u_4} [inst : MeasurableSpace G] [inst_1 : Sub G] {m : MeasurableSpace α}
  {mβ : MeasurableSpace β} [MeasurableSub₂ G] {f g : α → β → G} {h : α → β},
  Measurable ↿f → Measurable ↿g → Measurable h → Measurable fun a => (f a - g a) (h a)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
/-- For `s : ℝ`, the number of principal nonzero ideals in `𝓞 K` divisible par `J` of norm `≤ s`
multiplied by the order of the torsion of `K` is equal to the number of elements in `idealSet K J`
of norm `≤ s`.  -/
NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_dvd_norm_le : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (J : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) (s : ℝ),
  Nat.card { I // ↑J ∣ ↑I ∧ Submodule.IsPrincipal ↑I ∧ ↑(Ideal.absNorm ↑I) ≤ s } * NumberField.Units.torsionOrder K =
    Nat.card { a // NumberField.mixedEmbedding.norm ↑a ≤ s }
-- Mathlib.Geometry.Manifold.Diffeomorph
/-- `n`-times continuously differentiable diffeomorphism between `M` and `M'` with respect to `I`
and `I'`, denoted as `M ≃ₘ^n⟮I, I'⟯ M'` (in the `Manifold` namespace).  -/
Diffeomorph : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_5} →
                  [inst_5 : TopologicalSpace H] →
                    {H' : Type u_6} →
                      [inst_6 : TopologicalSpace H'] →
                        ModelWithCorners 𝕜 E H →
                          ModelWithCorners 𝕜 E' H' →
                            (M : Type u_9) →
                              [inst : TopologicalSpace M] →
                                [ChartedSpace H M] →
                                  (M' : Type u_10) →
                                    [inst : TopologicalSpace M'] →
                                      [ChartedSpace H' M'] → WithTop ℕ∞ → Type (max u_10 u_9)
-- Mathlib.Data.Bundle
/-- Natural embedding of the total space of `f *ᵖ E` into `B' × TotalSpace F E`.  -/
Bundle.pullbackTotalSpaceEmbedding : {B : Type u_1} →
  {F : Type u_2} →
    {E : B → Type u_3} → {B' : Type u_4} → (f : B' → B) → Bundle.TotalSpace F (f *ᵖ E) → B' × Bundle.TotalSpace F E
-- Mathlib.Algebra.Lie.Basis.Prod
_private.Mathlib.Algebra.Lie.Basis.Prod.0.LieAlgebra.Basis.prodF : {ι₁ : Type u_1} →
  {ι₂ : Type u_2} →
    {L₁ : Type u_3} →
      {L₂ : Type u_4} →
        [inst : Finite ι₁] →
          [inst_1 : Finite ι₂] →
            (eι : ι₁ ≃ ι₂) →
              [inst_2 : LieRing L₁] →
                [inst_3 : LieRing L₂] →
                  {R : Type u_5} →
                    [inst_4 : CommRing R] →
                      [inst_5 : LieAlgebra R L₁] →
                        {H₁ : LieSubalgebra R L₁} →
                          (b₁ : LieAlgebra.Basis ι₁ H₁) →
                            [inst_6 : LieAlgebra R L₂] →
                              {H₂ : LieSubalgebra R L₂} →
                                (b₂ : LieAlgebra.Basis ι₂ H₂) → ι₁ → ↥(LieAlgebra.Basis.prod✝ eι b₁ b₂)
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.initial_isEmpty : IsEmpty ↥(⊥_ AlgebraicGeometry.Scheme)
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence_inverse : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  (c : ComplexShape ι),
  (CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence C c).inverse =
    CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denoteAsIntModule.eq_1 : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (k : ℤ),
  Lean.Grind.CommRing.Poly.denoteAsIntModule ctx (Lean.Grind.CommRing.Poly.num k) = k • One.one
-- Mathlib.Data.List.Defs
/-- "Inhabited" `take` function: Take `n` elements from a list `l`. If `l` has less than `n`
elements, append `n - length l` elements `default`.  -/
List.takeI : {α : Type u_1} → [Inhabited α] → ℕ → List α → List α
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Left.pow_lt_one_iff : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : LinearOrder M] [MulLeftStrictMono M] {n : ℕ} {x : M},
  0 < n → (x ^ n < 1 ↔ x < 1)
-- Init.Data.String.Bootstrap
String.Internal.foldl : (String → Char → String) → String → String → String
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.functorProdFunctorEquivUnitIso_inv_app : ∀ (A : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  (C : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (X : CategoryTheory.Functor A B × CategoryTheory.Functor A C),
  (CategoryTheory.functorProdFunctorEquivUnitIso A B C).inv.app X =
    CategoryTheory.Prod.mkHom (X.1.prod'CompFst X.2).hom (X.1.prod'CompSnd X.2).hom
-- Mathlib.MeasureTheory.Order.Lattice
MeasurableInf₂.mk : ∀ {M : Type u_1} [inst : MeasurableSpace M] [inst_1 : Min M],
  autoParam (Measurable fun p => p.1 ⊓ p.2) MeasurableInf₂.measurable_inf._autoParam → MeasurableInf₂ M
-- Mathlib.Data.PFunctor.Multivariate.W
MvPFunctor.WPath.root.sizeOf_spec : ∀ {n : ℕ} {P : MvPFunctor.{u} (n + 1)} (a : P.A) (f : P.last.B a → P.last.W) (i : Fin2 n) (c : P.drop.B a i),
  sizeOf (MvPFunctor.WPath.root a f i c) = 1 + sizeOf a + sizeOf i + sizeOf c
-- Mathlib.Data.Quot
Quotient.instDecidableLiftOn₂OfDecidablePred_mathlib : {α : Sort u_1} →
  {β : Sort u_2} →
    {sa : Setoid α} →
      {sb : Setoid β} →
        (q₁ : Quotient sa) →
          (q₂ : Quotient sb) →
            (f : α → β → Prop) →
              (h : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂) →
                [(a : α) → DecidablePred (f a)] → Decidable (q₁.liftOn₂ q₂ f h)
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.nnnorm_eq_of_add_nnnorm_lt_max : ∀ {S : Type u_1} [inst : SeminormedAddGroup S] [IsUltrametricDist S] {x y : S}, ‖x + y‖₊ < max ‖x‖₊ ‖y‖₊ → ‖x‖₊ = ‖y‖₊
-- Std.Do.WP.Sound
_private.Std.Do.WP.Sound.0.Std.Do.EStateM.instWP.match_1.eq_2 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (e : ε) (s' : σ)
  (h_1 : (a : α) → (s' : σ) → motive (EStateM.Result.ok a s'))
  (h_2 : (e : ε) → (s' : σ) → motive (EStateM.Result.error e s')),
  (match EStateM.Result.error e s' with
    | EStateM.Result.ok a s' => h_1 a s'
    | EStateM.Result.error e s' => h_2 e s') =
    h_2 e s'
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.nextNum.eq_1 : ∀ {K : Type u_2} [inst : DivisionRing K] (a b ppredA predA : K),
  GenContFract.nextNum a b ppredA predA = b * predA + a * ppredA
-- Init.Data.SInt.Lemmas
ISize.ofIntLE_int8ToInt : ∀ (x : Int8), ISize.ofIntLE x.toInt ⋯ ⋯ = x.toISize
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.z : Std.Time.GenericFormat.DateBuilder✝ → Option String
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
/-- Coerce an arithmetic function with values in `ℕ` to one with values in `R`. We cannot inline
this in `natCoe` because it gets unfolded too much.  -/
ArithmeticFunction.natToArithmeticFunction : {R : Type u_1} → [inst : AddMonoidWithOne R] → ArithmeticFunction ℕ → ArithmeticFunction R
-- Aesop.Rule.Forward
Aesop.ForwardRule.mk.inj : ∀ {toForwardRuleInfo : Aesop.ForwardRuleInfo} {name : Aesop.RuleName} {term : Aesop.RuleTerm}
  {prio : Aesop.ForwardRulePriority} {toForwardRuleInfo_1 : Aesop.ForwardRuleInfo} {name_1 : Aesop.RuleName}
  {term_1 : Aesop.RuleTerm} {prio_1 : Aesop.ForwardRulePriority},
  { toForwardRuleInfo := toForwardRuleInfo, name := name, term := term, prio := prio } =
      { toForwardRuleInfo := toForwardRuleInfo_1, name := name_1, term := term_1, prio := prio_1 } →
    toForwardRuleInfo = toForwardRuleInfo_1 ∧ name = name_1 ∧ term = term_1 ∧ prio = prio_1
-- Mathlib.Data.PNat.Factors
PrimeMultiset.prod_inf : ∀ (u v : PrimeMultiset), (u ⊓ v).prod = u.prod.gcd v.prod
-- Std.Data.HashSet.Lemmas
Std.HashSet.ofList_eq_insertMany_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {l : List α}, Std.HashSet.ofList l = ∅.insertMany l
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValNat.div' : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ}, p.Coprime m → ∀ {b : ℕ}, m ∣ b → padicValNat p (b / m) = padicValNat p b
-- Init.Control.Basic
/-- Lifts an operation from an inner monad to an outer monad, providing it with a reverse lifting
operator that allows outer monad computations to be run in the inner monad. The lifted operation is
required to return extra information that is required in order to reconstruct the reverse lift's
effects in the outer monad; this extra information is determined by `stM`.

This function takes the inner monad as an implicit parameter. Use `controlAt` to specify it
explicitly.
 -/
control : {m : Type u → Type v} →
  {n : Type u → Type w} →
    [inst : MonadControlT m n] → [Bind n] → {α : Type u} → (({β : Type u} → n β → m (stM m n β)) → m (stM m n α)) → n α
-- Init.Data.Array.Erase
Array.erase_replicate_self : ∀ {α : Type u_1} [inst : BEq α] {n : ℕ} [LawfulBEq α] {a : α}, (Array.replicate n a).erase a = Array.replicate (n - 1) a
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- `SemilinearIsometryClass F σ E E₂` asserts `F` is a type of bundled `σ`-semilinear isometries
`E → E₂`.

See also `LinearIsometryClass F R E E₂` for the case where `σ` is the identity map on `R`.

A map `f` between an `R`-module and an `S`-module over a ring homomorphism `σ : R →+* S`
is semilinear if it satisfies the two properties `f (x + y) = f x + f y` and
`f (c • x) = (σ c) • f x`.  -/
SemilinearIsometryClass : (𝓕 : Type u_11) →
  {R : outParam (Type u_12)} →
    {R₂ : outParam (Type u_13)} →
      [inst : Semiring R] →
        [inst_1 : Semiring R₂] →
          outParam (R →+* R₂) →
            (E : outParam (Type u_14)) →
              (E₂ : outParam (Type u_15)) →
                [inst_2 : SeminormedAddCommGroup E] →
                  [inst_3 : SeminormedAddCommGroup E₂] → [Module R E] → [Module R₂ E₂] → [FunLike 𝓕 E E₂] → Prop
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Stmt.load : {K : Type u_1} →
  {Γ : K → Type u_2} → {Λ : Type u_3} → {σ : Type u_4} → (σ → σ) → Turing.TM2.Stmt Γ Λ σ → Turing.TM2.Stmt Γ Λ σ
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.FunIndParamKind : Type
-- Lean.Elab.PreDefinition.WF.Preprocess
/-- `let x : T := (wfParam e); body[x] ==> let x : T := e; body[wfParam y]` if `T` is not a proposition,
otherwise `... ==> let x : T := e; body[x]`. (Applies to `have`s too.)

Note: simprocs are provided the head of a let telescope, but not intermediate lets.
 -/
Lean.Elab.WF.paramLet : Lean.Meta.Simp.DSimproc
-- Mathlib.AlgebraicTopology.ModelCategory.Basic
/-- A model category is a category equipped with classes of morphisms named cofibrations,
fibrations and weak equivalences which satisfy the axioms CM1/CM2/CM3/CM4/CM5
of (closed) model categories.  -/
HomotopicalAlgebra.ModelCategory : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max u v)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.rightHomologyMap_op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasRightHomology] [inst_3 : S₂.HasRightHomology],
  (CategoryTheory.ShortComplex.rightHomologyMap φ).op =
    CategoryTheory.CategoryStruct.comp S₂.leftHomologyOpIso.inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ShortComplex.leftHomologyMap (CategoryTheory.ShortComplex.opMap φ)) S₁.leftHomologyOpIso.hom)
-- Init.Data.Array.Erase
_private.Init.Data.Array.Erase.0.Array.eraseIdxIfInBounds.eq_1 : ∀ {α : Type u} (xs : Array α) (i : ℕ), xs.eraseIdxIfInBounds i = if h : i < xs.size then xs.eraseIdx i h else xs
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.SimplicialObject.augmentedCechNerve_obj_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 :
    ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
      CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
  (f : CategoryTheory.Arrow C), (CategoryTheory.SimplicialObject.augmentedCechNerve.obj f).right = f.right
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafAdjunction.eq_1 : ∀ {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]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A],
  Φ.skyscraperPresheafAdjunction =
    CategoryTheory.Adjunction.mkOfHomEquiv
      { homEquiv := fun x x_1 => Φ.skyscraperPresheafHomEquiv, homEquiv_naturality_left_symm := ⋯,
        homEquiv_naturality_right := ⋯ }
-- Mathlib.Order.FixedPoints
OrderHom.map_lfp_comp : ∀ {α : Type u} {β : Type v} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : β →o α) (g : α →o β),
  f (OrderHom.lfp (g.comp f)) = OrderHom.lfp (f.comp g)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.leftRightHomologyComparison'_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₁.RightHomologyData)
  (h₁' : S₂.LeftHomologyData) (h₂' : S₂.RightHomologyData) {Z : C} (h : h₂'.H ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₁')
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁' h₂') h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap' φ h₂ h₂') h)
-- Mathlib.FieldTheory.AlgebraicClosure
/-- An element is contained in the algebraic closure of `F` in `E` if and only if
it is an integral element.  -/
mem_algebraicClosure_iff' : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x : E},
  x ∈ algebraicClosure F E ↔ IsIntegral F x
-- Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Polynomial.IsEisensteinAt.isWeaklyEisensteinAt : ∀ {R : Type u} [inst : CommSemiring R] {𝓟 : Ideal R} {f : Polynomial R}, f.IsEisensteinAt 𝓟 → f.IsWeaklyEisensteinAt 𝓟
-- Mathlib.Data.Seq.Basic
Stream'.Seq.join.eq_1 : ∀ {α : Type u},
  Stream'.Seq.join =
    Stream'.Seq.corec fun S =>
      match S.destruct with
      | none => none
      | some ((a, s), S') =>
        some
          (a,
            match s.destruct with
            | none => S'
            | some s' => Stream'.Seq.cons s' S')
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.insertMin.match_3.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : (t : Std.DTreeMap.Internal.Impl α β) → t.Balanced → Sort u_3) →
      (t : Std.DTreeMap.Internal.Impl α β) →
        (hr : t.Balanced) →
          ((hr : Std.DTreeMap.Internal.Impl.leaf.Balanced) → motive Std.DTreeMap.Internal.Impl.leaf hr) →
            ((sz : ℕ) →
                (k' : α) →
                  (v' : β k') →
                    (l' r' : Std.DTreeMap.Internal.Impl α β) →
                      (hr : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced) →
                        motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') hr) →
              motive t hr
-- Mathlib.Topology.Connected.Basic
preconnectedSpace_iff_univ : ∀ {α : Type u} [inst : TopologicalSpace α], PreconnectedSpace α ↔ IsPreconnected Set.univ
-- Lean.Server.CodeActions.Provider
/-- The return value of `findTactic?`.
This is the syntax for which code actions will be triggered.
 -/
Lean.CodeAction.FindTacticResult : Type
-- Mathlib.CategoryTheory.DifferentialObject
/-- A differential object in a category with zero morphisms and a shift is
an object `obj` equipped with
a morphism `d : obj ⟶ obj⟦1⟧`, such that `d^2 = 0`.  -/
CategoryTheory.DifferentialObject : (S : Type u_1) →
  [inst : AddMonoidWithOne S] →
    (C : Type u) →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [CategoryTheory.Limits.HasZeroMorphisms C] → [CategoryTheory.HasShift C S] → Type (max u v)
-- Mathlib.RingTheory.Flat.Basic
/-- If p and q are submodules of M and N respectively, and N and p are flat,
then `p ⊗ q → M ⊗ N` is injective.  -/
Module.Flat.tensorProduct_mapIncl_injective_of_left : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} {N : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (p : Submodule R M) (q : Submodule R N)
  [Module.Flat R ↥p] [Module.Flat R N], Function.Injective ⇑(TensorProduct.mapIncl p q)
-- Mathlib.Topology.MetricSpace.Isometry
/-- An isometry preserves distances.  -/
Isometry.dist_eq : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
  Isometry f → ∀ (x y : α), dist (f x) (f y) = dist x y
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
/-- `π` is an effective epimorphic family if there exists an `EffectiveEpiFamilyStruct` for `π`  -/
CategoryTheory.EffectiveEpiFamily.effectiveEpiFamily : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {B : C} {α : Type u_2} {X : α → C}
  {π : (a : α) → X a ⟶ B} [self : CategoryTheory.EffectiveEpiFamily X π],
  Nonempty (CategoryTheory.EffectiveEpiFamilyStruct X π)
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.le_ωSup_of_le : ∀ {α : Type u_2} [inst : OmegaCompletePartialOrder α] {c : OmegaCompletePartialOrder.Chain α} {x : α} (i : ℕ),
  x ≤ c i → x ≤ OmegaCompletePartialOrder.ωSup c
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.toNatIso_inv : ∀ {X Y : CategoryTheory.Cat} {F G : X ⟶ Y} (e : F ≅ G), (CategoryTheory.Cat.Hom.toNatIso e).inv = e.inv.toNatTrans
-- Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
CompletelyPositiveMap.mk.inj : ∀ {A₁ : Type u_1} {A₂ : Type u_2} {inst : NonUnitalCStarAlgebra A₁} {inst_1 : NonUnitalCStarAlgebra A₂}
  {inst_2 : PartialOrder A₁} {inst_3 : PartialOrder A₂} {inst_4 : StarOrderedRing A₁} {inst_5 : StarOrderedRing A₂}
  {toLinearMap : A₁ →ₗ[ℂ] A₂}
  {map_cstarMatrix_nonneg' : ∀ (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁), 0 ≤ M → 0 ≤ M.map ⇑toLinearMap}
  {toLinearMap_1 : A₁ →ₗ[ℂ] A₂}
  {map_cstarMatrix_nonneg'_1 : ∀ (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁), 0 ≤ M → 0 ≤ M.map ⇑toLinearMap_1},
  { toLinearMap := toLinearMap, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg' } =
      { toLinearMap := toLinearMap_1, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg'_1 } →
    toLinearMap = toLinearMap_1
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_subset_comm : ∀ {α : Type u_1} {s t u : Set α}, s \ t ⊆ u ↔ s \ u ⊆ t
-- Init.Data.List.Control
List.findSome?.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → Option β), List.findSome? f [] = none
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.core : Lean.Expr → Lean.Expr → Lean.Grind.AC.Expr → Lean.Grind.AC.Expr → Lean.Meta.Grind.AC.DiseqCnstrProof
-- Std.Data.TreeSet.Basic
/-- Removes the given key if it exists.  -/
Std.TreeSet.erase : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → α → Std.TreeSet α cmp
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Fin.accumulate_injective : ∀ {n m : ℕ}, n ≤ m → Function.Injective ⇑(Fin.accumulate n m)
-- Mathlib.Algebra.Group.Hom.Defs
/-- `MonoidHom` down-cast to a `MulHom`, forgetting the 1-preserving property.  -/
MonoidHom.coeToMulHom : {M : Type u_4} → {N : Type u_5} → [inst : MulOne M] → [inst_1 : MulOne N] → Coe (M →* N) (M →ₙ* N)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
preNormEDS_three : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R), preNormEDS b c d 3 = c
-- Mathlib.LinearAlgebra.TensorProduct.Tower
LinearEquiv.baseChange_zpow : ∀ (R : Type u_1) (A : Type u_2) (M : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (f : M ≃ₗ[R] M) (n : ℤ),
  LinearEquiv.baseChange R A M M (f ^ n) = LinearEquiv.baseChange R A M M f ^ n
-- Mathlib.RingTheory.PicardGroup
/-- The Picard group of a domain with normalizable gcd is trivial.
This includes unique factorization domains.  -/
instSubsingletonPicOfIsDomainOfIsGCDMonoid : ∀ (R : Type u_5) [inst : CommRing R] [IsDomain R] [IsGCDMonoid R], Subsingleton (CommRing.Pic R)
-- Lean.Setup
Lean.instInhabitedIRPhases : Inhabited Lean.IRPhases
-- Mathlib.Algebra.GroupWithZero.Pi
/-- The multiplicative homomorphism including a single `MulZeroClass`
into a dependent family of `MulZeroClass`es, as functions supported at a point.

This is the `MulHom` version of `Pi.single`.  -/
MulHom.single : {ι : Type u_1} →
  {α : ι → Type u_2} → [inst : (i : ι) → MulZeroClass (α i)] → [DecidableEq ι] → (i : ι) → α i →ₙ* (i : ι) → α i
-- Lean.LocalContext
/-- The unique id of the free variable.  -/
Lean.LocalDecl.fvarId : Lean.LocalDecl → Lean.FVarId
-- Mathlib.Algebra.Order.Ring.Synonym
OrderDual.instDistrib : {R : Type u_1} → [Distrib R] → Distrib Rᵒᵈ
-- Mathlib.Topology.Order.OrderClosed
Ioc_mem_nhdsLT : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {a b : α},
  a < b → Set.Ioc a b ∈ nhdsWithin b (Set.Iio b)
-- Init.Data.Array.Lemmas
Array.isEmpty_eq_false_iff : ∀ {α : Type u_1} {xs : Array α}, xs.isEmpty = false ↔ xs ≠ #[]
-- Init.Data.UInt.Lemmas
UInt8.lt_irrefl : ∀ (a : UInt8), ¬a < a
-- Mathlib.RingTheory.Ideal.Basis
Ideal.basisSpanSingleton_apply : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : CommSemiring R] [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra R S] (b : Module.Basis ι R S) {x : S} (hx : x ≠ 0) (i : ι),
  ↑((Ideal.basisSpanSingleton b hx) i) = x * b i
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.mk_zero_eq_addMonoidOf_mk : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} (x : M),
  AddLocalization.mk x 0 = (AddLocalization.addMonoidOf S) x
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.ext : ∀ {E : Type u_3} [inst : Group E] {p q : GroupSeminorm E}, (∀ (x : E), p x = q x) → p = q
-- Std.Internal.UV.System
Std.Internal.UV.System.RUsage.involuntaryCS : Std.Internal.UV.System.RUsage → UInt64
-- Mathlib.Tactic.NormNum.Basic
/-- The `norm_num` extension which identifies expressions of the form `¬a`,
such that `norm_num` successfully recognises `a`.  -/
Mathlib.Meta.NormNum.evalNot : Mathlib.Meta.NormNum.NormNumExt