mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.denote_combine_mul_k : ∀ (ctx : Int.Internal.Linear.Context) (a b : ℤ) (p₁ p₂ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.Poly.denote ctx (Int.Internal.Linear.Poly.combine_mul_k a b p₁ p₂) =
    a * Int.Internal.Linear.Poly.denote ctx p₁ + b * Int.Internal.Linear.Poly.denote ctx p₂
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens), AlgebraicGeometry.IsOpenImmersion U.ι
-- Std.Http.Protocol.H1.Parser
Std.Http.Protocol.H1.TakeResult.complete.injEq : ∀ (data data_1 : ByteSlice),
  (Std.Http.Protocol.H1.TakeResult.complete data = Std.Http.Protocol.H1.TakeResult.complete data_1) = (data = data_1)
-- Lean.CompactedRegion
Lean.instNonemptyCompactedRegion : Nonempty Lean.CompactedRegion
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Limits.PreservesBiproducts.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.PreservesZeroMorphisms],
  (∀ {J : Type w₁}, CategoryTheory.Limits.PreservesBiproductsOfShape J F) → CategoryTheory.Limits.PreservesBiproducts F
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rii.toList_iter : ∀ {α : Type u_1} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.Rxi.IsAlwaysFinite α] [inst_3 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rii α},
  r.iter.toList = r.toList
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.alter.match_1.eq_2 : ∀ {α : Type u_3} {β : α → Type u_1} (a : α) (motive : Option (β a) → Sort u_2) (b : β a) (h_1 : Unit → motive none)
  (h_2 : (b : β a) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.GroupTheory.Submonoid.Inverses
Submonoid.mul_leftInvEquiv : ∀ {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (x : ↥S.leftInv),
  ↑x * ↑((S.leftInvEquiv hS) x) = 1
-- Mathlib.Algebra.Group.Basic
eq_one_div_of_mul_eq_one_right : ∀ {α : Type u_1} [inst : DivisionMonoid α] {a b : α}, a * b = 1 → b = 1 / a
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_eq_getD_default : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited β] {a : α}, Std.DHashMap.Const.get! m a = Std.DHashMap.Const.getD m a default
-- Mathlib.Order.Partition.Basic
Partition.mk.congr_simp : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : α} (parts parts_1 : Set α) (e_parts : parts = parts_1)
  (sSupIndep' : sSupIndep parts) (bot_notMem' : ⊥ ∉ parts) (sSup_eq' : sSup parts = s),
  { parts := parts, sSupIndep' := sSupIndep', bot_notMem' := bot_notMem', sSup_eq' := sSup_eq' } =
    { parts := parts_1, sSupIndep' := ⋯, bot_notMem' := ⋯, sSup_eq' := ⋯ }
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
MeasureTheory.lintegral_le_iSup : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ]
  (f : α → ENNReal), ∫⁻ (x : α), f x ∂μ ≤ ⨆ x, f x
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- `piObj f` computes the product of a family of elements `f`.
(It is defined as an abbreviation for `limit (Discrete.functor f)`,
so for most facts about `piObj f`, you will just use general facts about limits.)  -/
CategoryTheory.Limits.piObj : {β : Type w} →
  {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (f : β → C) → [CategoryTheory.Limits.HasProduct f] → C
-- Mathlib.Analysis.RCLike.Basic
RCLike.toCompleteSpace : ∀ {K : semiOutParam (Type u_1)} [self : RCLike K], CompleteSpace K
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleRange_mk_zero : ∀ {n : ℕ} (h : 0 < n), ⟨0, h⟩.cycleRange = 1
-- Mathlib.Data.Fin.Tuple.Basic
Fin.cons.eq_1 : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u} (x : α 0) (p : (i : Fin n) → α i.succ) (j : Fin (n + 1)),
  Fin.cons x p j = Fin.cases x p j
-- Mathlib.Order.BoundedOrder.Basic
Prod.instBot : (α : Type u) → (β : Type v) → [Bot α] → [Bot β] → Bot (α × β)
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.instHasLimitObjFunctorConstTerminal : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasTerminal C],
  CategoryTheory.Limits.HasLimit ((CategoryTheory.Functor.const J).obj (⊤_ C))
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- `HasBinaryBiproduct P Q` expresses the mere existence of a bicone which is
simultaneously a limit and a colimit of the diagram `pair P Q`.  -/
CategoryTheory.Limits.HasBinaryBiproduct.exists_binary_biproduct : ∀ {C : Type uC} {inst : CategoryTheory.Category.{uC', uC} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {P Q : C} [self : CategoryTheory.Limits.HasBinaryBiproduct P Q],
  Nonempty (CategoryTheory.Limits.BinaryBiproductData P Q)
-- Mathlib.Algebra.Opposites
AddOpposite.exists : ∀ {α : Type u_1} {p : αᵃᵒᵖ → Prop}, (∃ a, p a) ↔ ∃ a, p (AddOpposite.op a)
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.coe_neg : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) (x : ↥s), ↑(-x) = -↑x
-- Mathlib.Algebra.Regular.ULift
ULift.isAddRegular_down : ∀ {R : Type v} [inst : Add R] {a : ULift.{u, v} R}, IsAddRegular a.down ↔ IsAddRegular a
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- This is a version of `exists_linearIndependent`
with an upper estimate on the size of the finite set we choose.  -/
Submodule.exists_finset_span_eq_linearIndepOn : ∀ (K : Type u_2) {M : Type u_3} [inst : DivisionRing K] [inst_1 : AddCommGroup M] [inst_2 : Module K M] (s : Set M)
  [Module.Finite K ↥(Submodule.span K s)],
  ∃ t,
    ↑t ⊆ s ∧
      t.card = Module.finrank K ↥(Submodule.span K s) ∧ Submodule.span K ↑t = Submodule.span K s ∧ LinearIndepOn K id ↑t
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.inv : ∀ {G : Type u_2} {α : Type u_3} [inst : Inv G] [inst_1 : MeasurableSpace G] [MeasurableInv G] {m : MeasurableSpace α}
  {f : α → G} {μ : MeasureTheory.Measure α}, AEMeasurable f μ → AEMeasurable f⁻¹ μ
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.setLAverage_congr_fun_ae : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f g : α → ENNReal},
  MeasurableSet s → (∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x) → ⨍⁻ (x : α) in s, f x ∂μ = ⨍⁻ (x : α) in s, g x ∂μ
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.evalEval_mul : ∀ {R : Type u_1} [inst : CommSemiring R] (x y : R) (p q : Polynomial (Polynomial R)),
  Polynomial.evalEval x y (p * q) = Polynomial.evalEval x y p * Polynomial.evalEval x y q
-- Lean.Parser.Command
Lean.Parser.Command.declVal.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Comonad.adj_unit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C),
  G.adj.unit = { app := fun X => { f := X.a, h := ⋯ }, naturality := ⋯ }
-- Lean.Parser.Term
Lean.Parser.Term.withDeclName.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Probability.Distributions.Poisson.Basic
/-- The sum of two independent Poisson random variables with rates `r₁, r₂` taking values in `R`
is a Poisson random variable with rate `r₁ + r₂`.  -/
ProbabilityTheory.IndepFun.hasLaw_add_map_cast_poissonMeasure : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] {mR : MeasurableSpace R} {Ω : Type u_2} {mΩ : MeasurableSpace Ω}
  {P : MeasureTheory.Measure Ω} [MeasurableAdd₂ R] {r₁ r₂ : NNReal} {X Y : Ω → R},
  ProbabilityTheory.IndepFun X Y P →
    ProbabilityTheory.HasLaw X (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure r₁)) P →
      ProbabilityTheory.HasLaw Y (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure r₂)) P →
        ProbabilityTheory.HasLaw (X + Y)
          (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure (r₁ + r₂))) P
-- Mathlib.Topology.UniformSpace.Basic
inhabitedUniformSpaceCore : {α : Type ua} → Inhabited (UniformSpace.Core α)
-- Mathlib.Data.Set.Function
/-- If `t ⊆ f '' s`, there exists a preimage of `t` under `f` contained in `s` such that
`f` restricted to `u` is injective.  -/
Set.SurjOn.exists_subset_injOn_image_eq : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β},
  Set.SurjOn f s t → ∃ u ⊆ s, Set.InjOn f u ∧ f '' u = t
-- Mathlib.CategoryTheory.Functor.Category
/-- The natural transformation `G.flip.obj Y ⟶ G'.flip.obj Y` induced by
a natural transformation `τ : G ⟶ G'` between bifunctors.  -/
CategoryTheory.NatTrans.flipApp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            {G G' : CategoryTheory.Functor C (CategoryTheory.Functor D E)} →
              (G ⟶ G') → (Y : D) → G.flip.obj Y ⟶ G'.flip.obj Y
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.mk.sizeOf_spec : ∀ (carrier : Type u) [str : AddGroup carrier],
  sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
AlgebraicIndependent.ne_zero : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  AlgebraicIndependent R x → ∀ [Nontrivial R] (i : ι), x i ≠ 0
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.mk : {M : Type u_1} →
  [inst : CommMonoid M] →
    {S : Submonoid M} →
      {N : Type u_2} →
        [inst_1 : CommMonoid N] → (toMulHom : M →ₙ* N) → S.IsLocalizationMap toMulHom.toFun → S.LocalizationMap N
-- Mathlib.Algebra.Lie.Subalgebra
LieModuleHom.coe_restrictLie : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (L' : LieSubalgebra R L)
  {M : Type w} [inst_3 : AddCommGroup M] [inst_4 : LieRingModule L M] {N : Type w₁} [inst_5 : AddCommGroup N]
  [inst_6 : LieRingModule L N] [inst_7 : Module R N] [inst_8 : Module R M] (f : M →ₗ⁅R,L⁆ N), ⇑(f.restrictLie L') = ⇑f
-- Init.Control.Basic
ForM.mk : {m : Type u → Type v} →
  {γ : Type w₁} → {α : outParam (Type w₂)} → (γ → (α → m PUnit.{u + 1}) → m PUnit.{u + 1}) → ForM m γ α
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.X_inj : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [Nontrivial R] (m n : σ),
  MvPolynomial.X m = MvPolynomial.X n ↔ m = n
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanILeanHeaderSetupInfoParams.mk : ℕ → Bool → Array Lean.Lsp.ImportInfo → Lean.Lsp.LeanILeanHeaderSetupInfoParams
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isSome_apply_of_mem_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Option γ} {k : α} (h : k ∈ Std.TreeMap.filterMap f t), (f (t.getKey k ⋯) t[k]).isSome = true
-- Mathlib.LinearAlgebra.Multilinear.Curry
/-- Given a linear map from `M p` to the space of multilinear maps
in `n` variables `M 0`, ..., `M n` with `M p` removed,
returns a multilinear map in all `n + 1` variables.  -/
LinearMap.uncurryMid : {R : Type uR} →
  {n : ℕ} →
    {M : Fin n.succ → Type v} →
      {M₂ : Type v₂} →
        [inst : CommSemiring R] →
          [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : Fin n.succ) → Module R (M i)] →
                [inst_4 : Module R M₂] →
                  (p : Fin (n + 1)) →
                    (M p →ₗ[R] MultilinearMap R (fun i => M (p.succAbove i)) M₂) → MultilinearMap R M M₂
-- Mathlib.Probability.Process.Predictable
MeasureTheory.IsStronglyPredictable.of_measurable_add_one : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {E : Type u_3} [inst : TopologicalSpace E] {𝓕 : MeasureTheory.Filtration ℕ m}
  {u : ℕ → Ω → E},
  MeasureTheory.StronglyMeasurable (u 0) →
    (∀ (n : ℕ), MeasureTheory.StronglyMeasurable (u (n + 1))) → MeasureTheory.IsStronglyPredictable 𝓕 u
-- Lean.Meta.Basic
Lean.Meta.instInhabitedCache.default : Lean.Meta.Cache
-- Mathlib.Data.Nat.Find
Nat.find_min : ∀ {p : ℕ → Prop} [inst : DecidablePred p] (H : ∃ n, p n) {m : ℕ}, m < Nat.find H → ¬p m
-- Init.Data.ByteArray.Basic
/-- Iterator over the bytes (`UInt8`) of a `ByteArray`.

Typically created by `arr.iter`, where `arr` is a `ByteArray`.

An iterator is *valid* if the position `i` is *valid* for the array `arr`, meaning `0 ≤ i ≤ arr.size`

Most operations on iterators return arbitrary values if the iterator is not valid. The functions in
the `ByteArray.Iterator` API should rule out the creation of invalid iterators, with two exceptions:

- `Iterator.next iter` is invalid if `iter` is already at the end of the array (`iter.atEnd` is
  `true`)
- `Iterator.forward iter n`/`Iterator.nextn iter n` is invalid if `n` is strictly greater than the
  number of remaining bytes.
 -/
ByteArray.Iterator : Type
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
/-- A fibrant resolution functor from a model category to the homotopy category
of fibrant objects.  -/
HomotopicalAlgebra.FibrantObject.HoCat.resolution : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] → CategoryTheory.Functor C (HomotopicalAlgebra.FibrantObject.HoCat C)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_neg : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} (f : α → G), ∫ (a : α), -f a ∂μ = -∫ (a : α), f a ∂μ
-- Mathlib.Data.Finset.Image
Finset.apply_coe_mem_map : ∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α) (x : ↥s), f ↑x ∈ Finset.map f s
-- Mathlib.RingTheory.Extension.Presentation.Basic
/-- If `algebraMap R S` is bijective, the empty generators are a presentation with no relations.  -/
Algebra.Presentation.ofBijectiveAlgebraMap : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          Function.Bijective ⇑(algebraMap R S) → Algebra.Presentation R S PEmpty.{w + 1} PEmpty.{t + 1}
-- Mathlib.Algebra.Algebra.Hom.Rat
RingEquiv.equivRatAlgEquiv_symm_apply : ∀ (R : Type u_1) (S : Type u_2) [inst : Ring R] [inst_1 : Ring S] [inst_2 : Algebra ℚ R] [inst_3 : Algebra ℚ S]
  (self : R ≃ₐ[ℚ] S), (RingEquiv.equivRatAlgEquiv R S).symm self = self.toRingEquiv
-- Mathlib.Algebra.Module.Submodule.Map
/-- The pullback of a submodule `p ⊆ M₂` along `f : M → M₂`  -/
Submodule.comap : {R : Type u_1} →
  {R₂ : Type u_3} →
    {M : Type u_5} →
      {M₂ : Type u_7} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R₂ M₂] → {σ₁₂ : R →+* R₂} → (M →ₛₗ[σ₁₂] M₂) → Submodule R₂ M₂ → Submodule R M
-- Init.Data.UInt.Lemmas
USize.toNat_mul : ∀ (a b : USize), (a * b).toNat = a.toNat * b.toNat % 2 ^ System.Platform.numBits
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constGetEntryLE?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Raw.Const.getEntryLE? t₁ k = Std.DTreeMap.Raw.Const.getEntryLE? t₂ k
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.mk.injEq : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S} {σ' : S →+* R}
  [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ] {M : Type u_3} [inst_4 : TopologicalSpace M]
  [inst_5 : AddCommMonoid M] {M₂ : Type u_4} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R M] [inst_9 : Module S M₂] (toLinearEquiv : M ≃ₛₗ[σ] M₂)
  (continuous_toFun : autoParam (Continuous (↑toLinearEquiv).toFun) ContinuousLinearEquiv.continuous_toFun._autoParam)
  (continuous_invFun : autoParam (Continuous toLinearEquiv.invFun) ContinuousLinearEquiv.continuous_invFun._autoParam)
  (toLinearEquiv_1 : M ≃ₛₗ[σ] M₂)
  (continuous_toFun_1 :
    autoParam (Continuous (↑toLinearEquiv_1).toFun) ContinuousLinearEquiv.continuous_toFun._autoParam)
  (continuous_invFun_1 :
    autoParam (Continuous toLinearEquiv_1.invFun) ContinuousLinearEquiv.continuous_invFun._autoParam),
  ({ toLinearEquiv := toLinearEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun } =
      { toLinearEquiv := toLinearEquiv_1, continuous_toFun := continuous_toFun_1,
        continuous_invFun := continuous_invFun_1 }) =
    (toLinearEquiv = toLinearEquiv_1)
-- Mathlib.Condensed.Functors
instFaithfulCondensedTypeCondensedSetUlift : Condensed.ulift.Faithful
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.single_length : ∀ {n : ℕ} (h : 0 < n), (Composition.single n h).length = 1
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- Restrict the codomain of a non-unital algebra homomorphism.  -/
NonUnitalAlgHom.codRestrict : {F : Type v'} →
  {R : Type u} →
    {A : Type v} →
      {B : Type w} →
        [inst : CommSemiring R] →
          [inst_1 : NonUnitalNonAssocSemiring A] →
            [inst_2 : Module R A] →
              [inst_3 : NonUnitalNonAssocSemiring B] →
                [inst_4 : Module R B] →
                  [inst_5 : FunLike F A B] →
                    [NonUnitalAlgHomClass F R A B] →
                      (f : F) → (S : NonUnitalSubalgebra R B) → (∀ (x : A), f x ∈ S) → A →ₙₐ[R] ↥S
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_false_of_clzAuxRec : ∀ {w n : ℕ} {x : BitVec w},
  (∀ (i : ℕ), n < i → x.getLsbD i = false) → ∀ (j : ℕ), x.getLsbD (w - (x.clzAuxRec n).toNat + j) = false
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.edgeSet_edge_subset : ∀ {V : Type u_1} {v w : V}, (SimpleGraph.edge v w).edgeSet ⊆ {s(v, w)}
-- Init.System.IOError
IO.Error.mkOtherError : UInt32 → String → IO.Error
-- Mathlib.RingTheory.Polynomial.Opposites
Polynomial.opRingEquiv_op_C_mul_X_pow : ∀ {R : Type u_1} [inst : Semiring R] (r : R) (n : ℕ),
  (Polynomial.opRingEquiv R) (MulOpposite.op (Polynomial.C r * Polynomial.X ^ n)) =
    Polynomial.C (MulOpposite.op r) * Polynomial.X ^ n
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.Iter.step_flatMapAfter.match_1.eq_2 : ∀ {α₂ γ : Type u_1} (motive : Option (Std.Iter γ) → Sort u_2) (it₂ : Std.Iter γ) (h_1 : Unit → motive none)
  (h_2 : (it₂ : Std.Iter γ) → motive (some it₂)),
  (match some it₂ with
    | none => h_1 ()
    | some it₂ => h_2 it₂) =
    h_2 it₂
-- Init.Data.Format.Basic
Std.Format.align.inj : ∀ {force force_1 : Bool}, Std.Format.align force = Std.Format.align force_1 → force = force_1
-- Batteries.Tactic.PrintOpaques
Batteries.Tactic.CollectOpaques.State.mk.inj : ∀ {visited : Lean.NameSet} {opaques : Array Lean.Name} {visited_1 : Lean.NameSet} {opaques_1 : Array Lean.Name},
  { visited := visited, opaques := opaques } = { visited := visited_1, opaques := opaques_1 } →
    visited = visited_1 ∧ opaques = opaques_1
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.expMap_apply : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.realSpace K)
  (w : NumberField.InfinitePlace K),
  ↑NumberField.mixedEmbedding.fundamentalCone.expMap x w = Real.exp ((↑w.mult)⁻¹ * x w)
-- Init.Data.Nat.Coprime
Nat.coprime_iff_gcd_eq_one : ∀ {m n : ℕ}, m.Coprime n ↔ m.gcd n = 1
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.pairwise_disjoint_addFundamentalInterior : ∀ (G : Type u_1) {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (s : Set α),
  Pairwise (Function.onFun Disjoint fun g => g +ᵥ MeasureTheory.addFundamentalInterior G s)
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
/-- Define a positive map from a linear map that maps nonnegative elements to nonnegative
elements  -/
PositiveLinearMap.mk₀ : {R : Type u_1} →
  {E₁ : Type u_2} →
    {E₂ : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : AddCommGroup E₁] →
          [inst_2 : PartialOrder E₁] →
            [IsOrderedAddMonoid E₁] →
              [inst_4 : AddCommGroup E₂] →
                [inst_5 : PartialOrder E₂] →
                  [IsOrderedAddMonoid E₂] →
                    [inst_7 : Module R E₁] →
                      [inst_8 : Module R E₂] → (f : E₁ →ₗ[R] E₂) → (∀ (x : E₁), 0 ≤ x → 0 ≤ f x) → E₁ →ₚ[R] E₂
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_finset_iff_measurable_set : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace β] {g : β → Finset α}, Measurable g ↔ Measurable fun x => ↑(g x)
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.liftRingHom_C : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {L : Type u_1} [inst_2 : Field L] (φ : Polynomial K →+* L)
  (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (x : K),
  (RatFunc.liftRingHom φ hφ) (RatFunc.C x) = φ (Polynomial.C x)
-- Mathlib.AlgebraicTopology.ModelCategory.Basic
HomotopicalAlgebra.ModelCategory.categoryWithFibrations : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    [self : HomotopicalAlgebra.ModelCategory C] → HomotopicalAlgebra.CategoryWithFibrations C
-- Mathlib.Combinatorics.SimpleGraph.Prod
_private.Mathlib.Combinatorics.SimpleGraph.Prod.0.SimpleGraph.Walk.ofBoxProdLeft.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} {x : α × β}
  (motive : (y : α × β) → (G □ H).Walk x y → Sort u_3) (y v : α × β) (h : (G □ H).Adj x v) (w : (G □ H).Walk v y)
  (h_1 : Unit → motive x SimpleGraph.Walk.nil)
  (h_2 : (y v : α × β) → (h : (G □ H).Adj x v) → (w : (G □ H).Walk v y) → motive y (SimpleGraph.Walk.cons h w)),
  (match y, SimpleGraph.Walk.cons h w with
    | .(x), SimpleGraph.Walk.nil => h_1 ()
    | y, SimpleGraph.Walk.cons h w => h_2 y v h w) =
    h_2 y v h w
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.Pairing.WeakRankFunction.mk : {X : SSet} →
  {A : X.Subcomplex} →
    {P : A.Pairing} →
      {α : Type v} →
        [inst : PartialOrder α] →
          (rank : ↑P.II → α) →
            (∀ {x y : ↑P.II}, P.AncestralRel x y → (↑x).dim = (↑y).dim → rank x < rank y) → P.WeakRankFunction α
-- Lean.Data.SSet
Lean.List.toSSet : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → List α → Lean.SSet α
-- Mathlib.GroupTheory.Submonoid.Inverses
AddSubmonoid.leftNeg_le_isAddUnit : ∀ {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M), S.leftNeg ≤ IsAddUnit.addSubmonoid M
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
/-- **Alias** of the forward direction of `MeasureTheory.Measure.FiniteAtFilter.inf_ae_iff`. -/
MeasureTheory.Measure.FiniteAtFilter.of_inf_ae : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α},
  μ.FiniteAtFilter (f ⊓ MeasureTheory.ae μ) → μ.FiniteAtFilter f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
/-- The power series expansion of `Real.cos`.  -/
Real.hasSum_cos : ∀ (r : ℝ), HasSum (fun n => (-1) ^ n * r ^ (2 * n) / ↑(2 * n).factorial) (Real.cos r)
-- Mathlib.Combinatorics.SimpleGraph.Operations
/-- Adjacency in `G.replaceVertex s t` which does not involve `t` is the same as that of `G`.  -/
SimpleGraph.adj_replaceVertex_iff_of_ne : ∀ {V : Type u_1} (G : SimpleGraph V) (s : V) {t : V} [inst : DecidableEq V] {v w : V},
  v ≠ t → w ≠ t → ((G.replaceVertex s t).Adj v w ↔ G.Adj v w)
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- Eta-expanded form of `Differentiable.inv` -/
Differentiable.fun_inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_5} [inst_3 : NormedDivisionRing R] [inst_4 : NormedAlgebra 𝕜 R] {h : E → R},
  Differentiable 𝕜 h → (∀ (x : E), h x ≠ 0) → Differentiable 𝕜 fun i => (h i)⁻¹