mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.match_1.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α)
  (motive : aig.BinaryRefVec w → Sort u_1) (lhs rhs : aig.RefVec w)
  (h_1 : (lhs rhs : aig.RefVec w) → motive { lhs := lhs, rhs := rhs }),
  (match { lhs := lhs, rhs := rhs } with
    | { lhs := lhs, rhs := rhs } => h_1 lhs rhs) =
    h_1 lhs rhs
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.toList_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {f : α → β → γ},
  (Std.TreeMap.Raw.map f t).toList = List.map (fun p => (p.1, f p.1 p.2)) t.toList
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.LiftRel.equiv : ∀ {α : Type u} (R : α → α → Prop), Equivalence R → Equivalence (Stream'.WSeq.LiftRel R)
-- Mathlib.Analysis.Convex.Side
Function.Injective.wOppSide_map_iff : ∀ {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [inst : CommRing R]
  [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V]
  [inst_5 : AddTorsor V P] [inst_6 : AddCommGroup V'] [inst_7 : Module R V'] [inst_8 : AddTorsor V' P']
  {s : AffineSubspace R P} {x y : P} {f : P →ᵃ[R] P'},
  Function.Injective ⇑f → ((AffineSubspace.map f s).WOppSide (f x) (f y) ↔ s.WOppSide x y)
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_union_le_eRk_add_eRk : ∀ {α : Type u_1} (M : Matroid α) (X Y : Set α), M.eRk (X ∪ Y) ≤ M.eRk X + M.eRk Y
-- Mathlib.RingTheory.Valuation.Basic
/-- The support of an additive valuation `v : R → Γ₀` is the ideal of `R` where `v x = ⊤`  -/
AddValuation.supp : {R : Type u_3} →
  {Γ₀ : Type u_4} → [inst : LinearOrderedAddCommMonoidWithTop Γ₀] → [inst_1 : CommRing R] → AddValuation R Γ₀ → Ideal R
-- Mathlib.Topology.Algebra.Module.Equiv
/-- A linear equivalence that is a homeomorphism is a continuous linear equivalence.  -/
ContinuousLinearEquiv.ofIsHomeomorph : {S : Type u_1} →
  [inst : Semiring S] →
    {S₁ : Type u_6} →
      {M : Type u_7} →
        {M₁ : Type u_8} →
          [inst_1 : Semiring S₁] →
            {σ : S →+* S₁} →
              {σ' : S₁ →+* S} →
                [inst_2 : RingHomInvPair σ σ'] →
                  [inst_3 : RingHomInvPair σ' σ] →
                    [inst_4 : TopologicalSpace M] →
                      [inst_5 : AddCommMonoid M] →
                        [inst_6 : Module S M] →
                          [inst_7 : TopologicalSpace M₁] →
                            [inst_8 : AddCommMonoid M₁] →
                              [inst_9 : Module S₁ M₁] → (f : M ≃ₛₗ[σ] M₁) → IsHomeomorph ⇑f → M ≃SL[σ] M₁
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.coe_inf : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] (S T : StarSubalgebra R A), ↑(S ⊓ T) = ↑S ∩ ↑T
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.CliqueFree.anti : ∀ {α : Type u_1} {G H : SimpleGraph α} {n : ℕ}, G ≤ H → H.CliqueFree n → G.CliqueFree n
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.diff.match_1.splitter : {α : Type u_1} →
  (motive : List α → List α → Sort u_2) →
    (x x_1 : List α) →
      ((l : List α) → motive l []) → ((l₁ : List α) → (a : α) → (l₂ : List α) → motive l₁ (a :: l₂)) → motive x x_1
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_obj : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (V : (↑U).Opens),
  (↑U).presheaf.obj (Opposite.op V) =
    X.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V))
-- Init.Prelude
/-- A reasoning principle for quotients that allows proofs about quotients to assume that all values are
constructed with `Quot.mk`.

`Quot.rec` is analogous to the [recursor](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=recursors) for a structure, and can
be used when the resulting type is not necessarily a proposition.

`Quot.ind` is a built-in primitive:
 * `Quot` is the built-in quotient type.
 * `Quot.mk` places elements of the underlying type `α` into the quotient.
 * `Quot.lift` allows the definition of functions from the quotient to some other type.
 * `Quot.sound` asserts the equality of elements related by `r`.
 -/
Quot.ind : ∀ {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop}, (∀ (a : α), β (Quot.mk r a)) → ∀ (q : Quot r), β q
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.range_ofENat : Set.range Cardinal.ofENat = Set.Iic Cardinal.aleph0
-- Mathlib.Data.Nat.BitIndices
Nat.notMem_bitIndices_self : ∀ (n : ℕ), n ∉ n.bitIndices
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
QuadraticModuleCat.forget₂_map : ∀ {R : Type u} [inst : CommRing R] (X Y : QuadraticModuleCat R) (f : X ⟶ Y),
  (CategoryTheory.forget₂ (QuadraticModuleCat R) (ModuleCat R)).map f =
    ModuleCat.ofHom (QuadraticModuleCat.Hom.toIsometry f).toLinearMap
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions : ∀ {P : TopCat → Prop} [inst : CompHausLike.HasExplicitFiniteCoproducts P]
  [CompHausLike.HasExplicitPullbacksOfInclusions P], CategoryTheory.FinitaryExtensive (CompHausLike P)
-- Mathlib.Algebra.Category.ModuleCat.Basic
/-- Turn a bilinear map into a homomorphism.  -/
ModuleCat.ofHom₂ : {R : Type u_1} → [inst : CommRing R] → {M N P : ModuleCat R} → (↑M →ₗ[R] ↑N →ₗ[R] ↑P) → (M ⟶ ModuleCat.of R (N ⟶ P))
-- Mathlib.Algebra.Group.Defs
/-- Any `CommMagma G` that satisfies `IsRightCancelMul G` also satisfies `IsLeftCancelMul G`.  -/
CommMagma.IsRightCancelMul.toIsLeftCancelMul : ∀ (G : Type u) [inst : CommMagma G] [IsRightCancelMul G], IsLeftCancelMul G
-- Lean.LocalContext
/-- The position of the decl in the local context.  -/
Lean.LocalDecl.index : Lean.LocalDecl → ℕ
-- Init.Data.Float.Float
/-- Obtains a `Float` whose value is near the given `UInt64`.

It will be exactly the value of the given `UInt64` if such a `Float` exists. If no such `Float`
exists, the returned value will either be the smallest `Float` that is larger than the given value,
or the largest `Float` that is smaller than the given value.

This function has a logical model in terms of `Float.Model`, but is overridden at runtime with an
efficient implementation.
 -/
UInt64.toFloat : UInt64 → Float
-- Mathlib.Data.Finset.Slice
Set.sized_iUnion : ∀ {α : Type u_1} {ι : Sort u_2} {r : ℕ} {f : ι → Set (Finset α)}, Set.Sized r (⋃ i, f i) ↔ ∀ (i : ι), Set.Sized r (f i)
-- Mathlib.Order.RelIso.Set
RelIso.preimage_eq_image_symm : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) (t : Set β), ⇑e ⁻¹' t = ⇑e.symm '' t
-- Mathlib.GroupTheory.DivisibleHull
/-- Define coercion as `m ↦ m / 1`.  -/
DivisibleHull.coe : {M : Type u_1} → [inst : AddCommMonoid M] → M → DivisibleHull M
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPolynomial.coe_mul : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (φ ψ : MvPolynomial σ R), ↑(φ * ψ) = ↑φ * ↑ψ
-- Mathlib.GroupTheory.Divisible
DivisibleBy.div_zero : ∀ {A : Type u_1} {α : Type u_2} {inst : AddMonoid A} {inst_1 : SMul α A} {inst_2 : Zero α} [self : DivisibleBy A α]
  (a : A), DivisibleBy.div a 0 = 0
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `AnalyticOnNhd.const_smul` -/
AnalyticOnNhd.fun_const_smul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E}
  {R : Type u_9} [inst_5 : NormedRing R] [inst_6 : Module R F] [IsBoundedSMul R F] [SMulCommClass 𝕜 R F] {c : R},
  AnalyticOnNhd 𝕜 f s → AnalyticOnNhd 𝕜 (fun i => c • f i) s
-- Mathlib.Order.BooleanAlgebra.Set
Set.mem_of_mem_sdiff : ∀ {α : Type u_1} {s t : Set α} {x : α}, x ∈ s \ t → x ∈ s
-- Lean.DocString.Types
Lean.Doc.instOrdDescItem.ord : {α : Type u_1} → {β : Type u_2} → [Ord α] → [Ord β] → Lean.Doc.DescItem α β → Lean.Doc.DescItem α β → Ordering
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sin_sq_add_cos_sq : ∀ (x : ℂ), Complex.sin x ^ 2 + Complex.cos x ^ 2 = 1
-- Mathlib.Algebra.Homology.HomotopyCategory
HomotopyCategory.instInhabitedOfHasZeroObject : {ι : Type u_2} →
  (V : Type u) →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        (c : ComplexShape ι) → [CategoryTheory.Limits.HasZeroObject V] → Inhabited (HomotopyCategory V c)
-- Std.Time.Zoned.Database.TzIf
_private.Std.Time.Zoned.Database.TzIf.0.Std.Time.TimeZone.TZif.termInt64 : Lean.ParserDescr
-- Mathlib.Order.Defs.LinearOrder
Ordering.Compares.eq_2 : ∀ {α : Type u_1} [inst : LT α] (x x_1 : α), Ordering.eq.Compares x x_1 = (x = x_1)
-- Mathlib.SetTheory.Cardinal.Finite
Nat.finite_of_card_ne_zero : ∀ {α : Type u_1}, Nat.card α ≠ 0 → Finite α
-- Mathlib.GroupTheory.Sylow
Sylow.subtype_injective : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {N : Subgroup G} {P Q : Sylow p G} {hP : ↑P ≤ N} {hQ : ↑Q ≤ N},
  P.subtype hP = Q.subtype hQ → P = Q
-- Mathlib.Algebra.Category.Grp.Yoneda
AddCommGrpCat.coyoneda_obj_map : ∀ (M : AddCommGrpCatᵒᵖ) {X Y : AddCommGrpCat} (f : X ⟶ Y),
  (AddCommGrpCat.coyoneda.obj M).map f = AddCommGrpCat.ofHom (AddMonoidHom.compHom (AddCommGrpCat.Hom.hom f))
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.commRing : {R : Type u} → [inst : CommRing R] → (self : CommAlgCat R) → CommRing ↑self
-- Mathlib.Data.List.Sublists
List.sublists'_cons : ∀ {α : Type u} (a : α) (l : List α), (a :: l).sublists' = l.sublists' ++ List.map (List.cons a) l.sublists'
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cone.extendComp`.

---

Extending a cone by a composition is the same as extending the cone twice.  -/
CategoryTheory.Limits.Cones.extendComp : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (s : CategoryTheory.Limits.Cone F) →
            {X Y : C} →
              (f : X ⟶ Y) → (g : Y ⟶ s.pt) → s.extend (CategoryTheory.CategoryStruct.comp f g) ≅ (s.extend g).extend f
-- Batteries.Data.List.Lemmas
List.cons_diff : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) (l₁ l₂ : List α),
  (a :: l₁).diff l₂ = if a ∈ l₂ then l₁.diff (l₂.erase a) else a :: l₁.diff l₂
-- Lean.ToExpr
/-- We use the `ToExpr` type class to convert values of type `α` into
expressions that denote these values in Lean.

Examples:
```
toExpr true = .const ``Bool.true []

toTypeExpr Bool = .const ``Bool []
```

See also `ToLevel` for representing universe levels as `Level` expressions.
 -/
Lean.ToExpr : Type u → Type u
-- Mathlib.RingTheory.Ideal.MonicSpan
Polynomial.exists_monic_span : ∀ {k : Type u_2} [inst : Field k] (I : Ideal (Polynomial k)), I ≠ ⊥ → ∃ f, f.Monic ∧ I = Ideal.span {f}
-- Mathlib.Analysis.Convex.Basic
convex_multiset_sum : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s : Multiset (Set E)}, (∀ i ∈ s, Convex 𝕜 i) → Convex 𝕜 s.sum
-- Mathlib.Order.Max
/-- For each term `a`, there is some `b` which is either incomparable or strictly larger.  -/
NoTopOrder.exists_not_le : ∀ {α : Type u_3} {inst : LE α} [self : NoTopOrder α] (a : α), ∃ b, ¬b ≤ a
-- Mathlib.Data.Fin.SuccPred
/-- Sending `Fin (n+1)` to `Fin n` by subtracting one from anything above `p`
then back to `Fin (n+1)` with a gap around `p.succ` is the identity away from `p.succ`.  -/
Fin.succ_succAbove_predAbove : ∀ {n : ℕ} {p : Fin n} {i : Fin (n + 1)}, i ≠ p.succ → p.succ.succAbove (p.predAbove i) = i
-- Mathlib.Data.Seq.Basic
Stream'.Seq.toList.congr_simp : ∀ {α : Type u} (s s_1 : Stream'.Seq α) (e_s : s = s_1) (h : s.Terminates), s.toList h = s_1.toList ⋯
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_enorm_iff : ∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {f : α → ε},
  MeasureTheory.AEStronglyMeasurable f μ → (MeasureTheory.Integrable (fun x => ‖f x‖ₑ) μ ↔ MeasureTheory.Integrable f μ)
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.domDomCongrₗ_symm_apply : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {ι' : Type u_8} (S : Type u_12) [inst_5 : Semiring S]
  [inst_6 : Module S N] [inst_7 : SMulCommClass R S N] (σ : ι ≃ ι') (f : M [⋀^ι']→ₗ[R] N),
  (AlternatingMap.domDomCongrₗ S σ).symm f = AlternatingMap.domDomCongr σ.symm f
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
/-- Sum of a multiset given a commutative additive monoid structure on `M`.
`sum {a, b, c} = a + b + c`  -/
Multiset.sum : {M : Type u_3} → [AddCommMonoid M] → Multiset M → M
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_filter_key : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → Bool} {k : α}, k ∈ Std.ExtDTreeMap.filter (fun a x => f a) t ↔ ∃ (h : k ∈ t), f (t.getKey k h) = true
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.δ_comp_yonedaEquiv_symm : ∀ {X : SSet} {n : ℕ} (x : X.obj (Opposite.op { len := n + 1 })) (i : Fin (n + 2)),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i) (SSet.yonedaEquiv.symm x) =
    SSet.yonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X i)) x)
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂_obj_obj_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (G k j : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂ C).obj G).obj k).obj j =
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj j G) k
-- Mathlib.Algebra.Group.Torsion
self_eq_neg : ∀ {G : Type u_2} [inst : AddGroup G] [IsAddTorsionFree G] {a : G}, a = -a ↔ a = 0
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_mul_const_Ioi₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {c : G₀} (a : G₀),
  0 < c → (fun x => x * c) ⁻¹' Set.Ioi a = Set.Ioi (a / c)
-- Mathlib.GroupTheory.GroupAction.Hom
MulSemiringActionHom.map_smul : ∀ {M : Type u_1} [inst : Monoid M] {R : Type u_10} [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R]
  {S : Type u_12} [inst_3 : Semiring S] [inst_4 : MulSemiringAction M S] (f : R →+*[M] S) (m : M) (x : R),
  f (m • x) = m • f x
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
IsAddIndecomposable.image_baseOf_neg_comp_eq : ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : AddCommGroup G] [inst_1 : LinearOrder S]
  [inst_2 : InvolutiveNeg ι] [inst_3 : AddCommGroup S] [IsOrderedAddMonoid S] (v : ι → G),
  (∀ (i : ι), v (-i) = -v i) →
    ∀ (f : G →+ S),
      v '' IsAddIndecomposable.baseOf v (negAddMonoidHom.comp f) =
        ⇑negAddMonoidHom ∘ v '' IsAddIndecomposable.baseOf v f
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_right_le_mk_sub : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a b : M},
  ArchimedeanClass.mk b ≤ ArchimedeanClass.mk a → ArchimedeanClass.mk b ≤ ArchimedeanClass.mk (a - b)
-- Mathlib.RingTheory.Extension.Presentation.Submersive
/-- If `S = 0`, this is the submersive presentation on one generator and one relation.  -/
Algebra.SubmersivePresentation.ofSubsingleton : (R : Type u) →
  (S : Type v) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] → [Subsingleton S] → Algebra.SubmersivePresentation R S PUnit.{u_2 + 1} PUnit.{u_1 + 1}
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.instInhabitedEqCnstr : Inhabited Lean.Meta.Grind.Arith.Linear.EqCnstr
-- Mathlib.AlgebraicGeometry.Sites.Affine
AlgebraicGeometry.Scheme.affineOverMk_hom : ∀ {S : AlgebraicGeometry.Scheme} {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {R : CommRingCat}
  (f : AlgebraicGeometry.Spec R ⟶ S) (hf : P f), (AlgebraicGeometry.Scheme.affineOverMk f hf).hom = f
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
/-- The "clifford conjugate" maps to the quaternion conjugate.  -/
CliffordAlgebraQuaternion.toQuaternion_star : ∀ {R : Type u_1} [inst : CommRing R] {c₁ c₂ : R} (c : CliffordAlgebra (CliffordAlgebraQuaternion.Q c₁ c₂)),
  CliffordAlgebraQuaternion.toQuaternion (star c) = star (CliffordAlgebraQuaternion.toQuaternion c)
-- Aesop.Stats.Basic
Aesop.ForwardClusterStateStats : Type
-- Mathlib.Topology.LocalAtTarget
Set.restrictPreimage_isOpenEmbedding : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} (s : Set β),
  Topology.IsOpenEmbedding f → Topology.IsOpenEmbedding (s.restrictPreimage f)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.toRingHom_mapDomainRingEquiv : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : AddMonoid M] [inst_2 : AddMonoid N]
  (e : M ≃+ N), (AddMonoidAlgebra.mapDomainRingEquiv R e).toRingHom = AddMonoidAlgebra.mapDomainRingHom R ↑e
-- Mathlib.CategoryTheory.Products.Basic
/-- The counit isomorphism for `functorProdFunctorEquiv`  -/
CategoryTheory.functorProdFunctorEquivCounitIso : (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] →
            (CategoryTheory.functorProdToProdFunctor A B C).comp (CategoryTheory.prodFunctorToFunctorProd A B C) ≅
              CategoryTheory.Functor.id (CategoryTheory.Functor A (B × C))
-- Mathlib.Topology.NhdsWithin
tendsto_nhdsWithin_range : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {a : α} {l : Filter β} {f : β → α},
  Filter.Tendsto f l (nhdsWithin a (Set.range f)) ↔ Filter.Tendsto f l (nhds a)
-- Lean.Elab.Tactic.Rewrite
Lean.Elab.Tactic.rewriteLocalDecl : Lean.Syntax → Bool → Lean.FVarId → optParam Lean.Meta.Rewrite.Config { } → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
LinearIndependent.lt_aleph0_of_finiteDimensional : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type w}
  [FiniteDimensional K V] {v : ι → V}, LinearIndependent K v → Cardinal.mk ι < Cardinal.aleph0
-- Mathlib.LinearAlgebra.Dual.Basis
/-- `e` and `ε` have characteristic properties of a basis and its dual  -/
Module.DualBases : {R : Type u_1} →
  {M : Type u_2} →
    {ι : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (ι → M) → (ι → Module.Dual R M) → Prop
-- Lean.Meta.Match.Basic
Lean.Meta.Match.instInhabitedAltLHS : Inhabited Lean.Meta.Match.AltLHS
-- Init.Data.List.Sublist
List.prefix_append : ∀ {α : Type u_1} (l₁ l₂ : List α), l₁ <+: l₁ ++ l₂
-- Mathlib.Computability.NFA
NFA.disjoint_stepSet_reverse : ∀ {α : Type u} {σ : Type v} {M : NFA α σ} {a : α} {S S' : Set σ},
  Disjoint S (M.reverse.stepSet S' a) ↔ Disjoint S' (M.stepSet S a)
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- Quotients of locally path-connected spaces are locally path-connected.  -/
Quot.locallyPathConnectedSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyPathConnectedSpace X] {r : X → X → Prop},
  LocallyPathConnectedSpace (Quot r)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rcc_eq_singleton : ∀ {m n : ℕ}, n = m → (m...=n).toList = [m]
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiable.snd : ∀ {𝕜 : 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'] {F : Type u_11}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_12} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_13} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {f : N → M × M'}, MDiff f → MDiff fun x => (f x).2
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.piPremeasure_pi' : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] {m : (i : ι) → MeasureTheory.OuterMeasure (α i)}
  {s : (i : ι) → Set (α i)}, MeasureTheory.piPremeasure m (Set.univ.pi s) = ∏ i, (m i) (s i)
-- Init.Data.Int.Linear
Int.Internal.Linear.diseq_norm_poly : ∀ (ctx : Int.Internal.Linear.Context) (p p' : Int.Internal.Linear.Poly),
  Int.Internal.Linear.Poly.denote' ctx p = Int.Internal.Linear.Poly.denote' ctx p' →
    Int.Internal.Linear.Poly.denote' ctx p ≠ 0 → Int.Internal.Linear.Poly.denote' ctx p' ≠ 0
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
/-- Given the data of a constructible set `s`, namely finitely many tuples `(f, g₁, ..., gₙ)` such
that `s = ⋃ (f, g₁, ..., gₙ), V(g₁, ..., gₙ) \ V(f)`, return `s`.  -/
PrimeSpectrum.ConstructibleSetData.toSet : {R : Type u_1} → [inst : CommSemiring R] → PrimeSpectrum.ConstructibleSetData R → Set (PrimeSpectrum R)
-- Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.State.mk : Array Lean.MVarId → List (Lean.TSyntax `rintroPat) → Mathlib.Tactic.GCongr.State
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
/-- If `μ 1 ≤ 1` and `μ` is nonarchimedean, then `smoothingFun μ` is
power-multiplicative.  -/
isPowMul_smoothingFun : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R), μ 1 ≤ 1 → IsPowMul (smoothingFun μ)
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.leftAdjointUniq.eq_1 : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj1 : F ⊣ G) (adj2 : F' ⊣ G),
  adj1.leftAdjointUniq adj2 = ((CategoryTheory.conjugateIsoEquiv adj1 adj2).symm (CategoryTheory.Iso.refl G)).symm
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- **Alias** of `AlgHom.equivFieldRange_apply_coe`. -/
AlgHom.equivFieldRange_apply : ∀ {K : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
  [inst_3 : Algebra K L] [inst_4 : Algebra K L'] (f : L →ₐ[K] L') (a : L), ↑(f.equivFieldRange a) = f a
-- Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
SSet.instRespectsIsoInnerFibrations : SSet.innerFibrations.RespectsIso
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instIsCentralScalar : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} {A : Type u_5} [inst : SMul R A] [inst_1 : SMul Rᵐᵒᵖ A]
  [IsCentralScalar R A], IsCentralScalar R (CStarMatrix m n A)
-- Mathlib.Algebra.Polynomial.Derivative
/-- Iterated derivatives as a finite support function.
 -/
Polynomial.derivativeFinsupp : {R : Type u} → [inst : Semiring R] → Polynomial R →ₗ[R] ℕ →₀ Polynomial R
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.prod_leftUnitor_hom_snd : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] {a b : B × C}
  (f : a ⟶ b), (CategoryTheory.Bicategory.leftUnitor f).hom.2 = (CategoryTheory.Bicategory.leftUnitor f.2).hom
-- Mathlib.Order.GameAdd
Acc.sym2_gameAdd : ∀ {α : Type u_1} {rα : α → α → Prop} {a b : α}, Acc rα a → Acc rα b → Acc (Sym2.GameAdd rα) s(a, b)
-- Mathlib.Order.Filter.CountablyGenerated
Filter.isCountablyGenerated_principal : ∀ {α : Type u_1} (s : Set α), (Filter.principal s).IsCountablyGenerated
-- Lean.Expr
Lean.instBEqFVarId : BEq Lean.FVarId
-- Mathlib.Analysis.Complex.IntegerCompl
_private.Mathlib.Analysis.Complex.IntegerCompl.0.Complex.termℂ_ℤ : Lean.ParserDescr