mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
midpoint_le_midpoint : ∀ {k : Type u_1} {E : Type u_2} [inst : Ring k] [inst_1 : LinearOrder k] [IsStrictOrderedRing k]
  [inst_3 : AddCommGroup E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E]
  [IsStrictOrderedModule k E] {a a' b b' : E} [inst_8 : Invertible 2],
  a ≤ a' → b ≤ b' → midpoint k a b ≤ midpoint k a' b'
-- Batteries.Data.Float.Basic
/-- Returns `v, exp` integers such that `f = v * 2^exp`.
Like `toRatParts`, but `e` is guaranteed to be minimal (`v` is always odd), unless `v = 0`.
`v.abs` will be at most `2^24 - 1` because `Float32` has 24 bits of precision.
Returns `none` when `f` is not finite (i.e. `inf`, `-inf` or a `nan`).  -/
Float32.toRatParts' : Float32 → Option (ℤ × ℤ)
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.evaln.match_1.eq_5 : ∀ (motive : ℕ → Nat.Partrec.Code → Sort u_1) (k : ℕ) (h_1 : (x : Nat.Partrec.Code) → motive 0 x)
  (h_2 : (k : ℕ) → motive k.succ Nat.Partrec.Code.zero) (h_3 : (k : ℕ) → motive k.succ Nat.Partrec.Code.succ)
  (h_4 : (k : ℕ) → motive k.succ Nat.Partrec.Code.left) (h_5 : (k : ℕ) → motive k.succ Nat.Partrec.Code.right)
  (h_6 : (k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.pair cg))
  (h_7 : (k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.comp cg))
  (h_8 : (k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.prec cg))
  (h_9 : (k : ℕ) → (cf : Nat.Partrec.Code) → motive k.succ cf.rfind'),
  (match k.succ, Nat.Partrec.Code.right with
    | 0, x => h_1 x
    | k.succ, Nat.Partrec.Code.zero => h_2 k
    | k.succ, Nat.Partrec.Code.succ => h_3 k
    | k.succ, Nat.Partrec.Code.left => h_4 k
    | k.succ, Nat.Partrec.Code.right => h_5 k
    | k.succ, cf.pair cg => h_6 k cf cg
    | k.succ, cf.comp cg => h_7 k cf cg
    | k.succ, cf.prec cg => h_8 k cf cg
    | k.succ, cf.rfind' => h_9 k cf) =
    h_5 k
-- Mathlib.Data.Matrix.Mul
sumElim_dotProduct_sumElim : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : NonUnitalNonAssocSemiring α] (u v : m → α) (x y : n → α), Sum.elim u x ⬝ᵥ Sum.elim v y = u ⬝ᵥ v + x ⬝ᵥ y
-- Mathlib.NumberTheory.Multiplicity
Nat.emultiplicity_pow_add_pow : ∀ {p : ℕ},
  Nat.Prime p →
    Odd p →
      ∀ {x y : ℕ},
        p ∣ x + y →
          ¬p ∣ x → ∀ {n : ℕ}, Odd n → emultiplicity p (x ^ n + y ^ n) = emultiplicity p (x + y) + emultiplicity p n
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.sum_const : ∀ (ι : Type u) (a : Cardinal.{v}),
  (Cardinal.sum fun x => a) = Cardinal.lift.{v, u} (Cardinal.mk ι) * Cardinal.lift.{u, v} a
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
/-- If `R → A → B` is an algebra tower, `C` is the integral closure of `R` in `B`
and `A` is integral over `R`, then `C` is the integral closure of `A` in `B`.  -/
IsIntegralClosure.tower_top : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {B : Type u_6}
  {C : Type u_7} [inst_3 : CommSemiring C] [inst_4 : CommRing B] [inst_5 : Algebra R B] [inst_6 : Algebra A B]
  [inst_7 : Algebra C B] [IsScalarTower R A B] [IsIntegralClosure C R B] [Algebra.IsIntegral R A],
  IsIntegralClosure C A B
-- Mathlib.LinearAlgebra.Matrix.ZMatrix
/-- A spectral bound result for Z-matrices satisfying a positive-definiteness condition.

It is important because it applies to Cartan matrices, and shows that all (real) eigenvalues must
be strictly less than 4 (a fact which is necessary in the proof of
`RootPairing.GeckConstruction.instIsIrreducible`).  -/
Matrix.lt_two_mul_of_mul_diagonal_posDef_of_for_le_of_hasEigen : ∀ {ι : Type u_1} {R : Type u_2} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : CommRing R]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] [inst_5 : StarRing R] [TrivialStar R] (A : Matrix ι ι R) (d : ι → R),
  (Matrix.diagonal d * A).PosDef →
    (∀ (i : ι), 0 < d i) →
      ∀ (μ ρ : R),
        (∀ (i j : ι), A i j ≤ if i = j then μ else 0) → Module.End.HasEigenvalue (Matrix.toLin' A) ρ → ρ < 2 * μ
-- Mathlib.Analysis.LocallyConvex.HahnBanach
/-- **Hahn-Banach theorem** for continuous linear functionals on polynormable spaces over a field
satisfying `IsRCLikeNormedField`.  -/
StrongDual.exists_extension : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] {𝕜 : Type u_3}
  [inst_2 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_4 : Module 𝕜 E] [PolynormableSpace 𝕜 E]
  (S : Submodule 𝕜 E) (f : StrongDual 𝕜 ↥S), ∃ g, ∀ (x : ↥S), g ↑x = f x
-- Lean.Environment
/-- The module data that should be used for server purposes.  -/
_private.Lean.Environment.0.Lean.ImportedModule.serverData? : Lean.ImportedModule✝ → Lean.OLeanLevel → Option Lean.ModuleData
-- Mathlib.Analysis.Normed.Group.Basic
mem_sphere_iff_norm_neg_add_eq : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {a b : E} {r : ℝ}, b ∈ Metric.sphere a r ↔ ‖-b + a‖ = r
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_toAddSubmonoid' : ∀ {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₂}
  [inst_6 : RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M),
  (Submodule.map f p).toAddSubmonoid = AddSubmonoid.map f p.toAddSubmonoid
-- Mathlib.Algebra.Group.Prod
Prod.instLeftCancelMonoid : {M : Type u_3} → {N : Type u_4} → [LeftCancelMonoid M] → [LeftCancelMonoid N] → LeftCancelMonoid (M × N)
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
/-- Homs in `SimplexCategory` are equivalent to functors between finite linear orders.  -/
SimplexCategory.homEquivFunctor : {a b : SimplexCategory} → (a ⟶ b) ≃ CategoryTheory.Functor (Fin (a.len + 1)) (Fin (b.len + 1))
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- Equality holds when `b ≠ 0`. See `inv_mul_cancel_right`.  -/
le_inv_mul_right : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : Preorder G₀] {a b : G₀}, a ≤ 0 → a ≤ a * b⁻¹ * b
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_modify_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {f : β → β}, (t.modify k f).getKey! k = if k ∈ t then k else default
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.Products.instWellFoundedLT : ∀ {I : Type u} [inst : LinearOrder I] [WellFoundedLT I], WellFoundedLT (Profinite.NobelingProof.Products I)
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
/-- The object part of the initial functor `ℕᵒᵖ ⥤ J`  -/
CategoryTheory.Limits.IsFiltered.sequentialFunctor_obj : (J : Type u_2) → [Countable J] → [inst : Preorder J] → [CategoryTheory.IsFiltered J] → ℕ → J
-- Init.Data.List.MinMax
List.isSome_min?_of_ne_nil : ∀ {α : Type u_1} [inst : Min α] {l : List α}, l ≠ [] → l.min?.isSome = true
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.zpow'.eq_1 : ∀ {α : Type u_1} [inst : GroupWithZero α] (a : α) (n : ℤ),
  Mathlib.Tactic.FieldSimp.zpow' a n = if a = 0 ∧ n = 0 then 0 else a ^ n
-- Mathlib.Geometry.Euclidean.Angle.Incenter
/-- A point lying on the internal angle bisector from vertex `i₁` and the external angle bisector
from another vertex is the excenter opposite vertex `i₁`.  -/
Affine.Triangle.eq_excenter_singleton_of_oangle_eq_of_oangle_eq_add_pi : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {t : Affine.Triangle ℝ P} {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ →
      i₂ ≠ i₃ →
        ∀ {p : P},
          EuclideanGeometry.oangle (t.points i₂) (t.points i₁) p =
              EuclideanGeometry.oangle p (t.points i₁) (t.points i₃) →
            EuclideanGeometry.oangle (t.points i₃) (t.points i₂) p =
                EuclideanGeometry.oangle p (t.points i₂) (t.points i₁) + ↑Real.pi →
              p = Affine.Simplex.excenter t {i₁}
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
/-- Constant zero function has sum `0`  -/
hasSum_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β},
  HasSum (fun x => 0) 0 L
-- Mathlib.Algebra.Ring.Periodic
/-- A function `f` is said to be `Periodic` with period `c` if for all `x`, `f (x + c) = f x`.  -/
Function.Periodic : {α : Type u_1} → {β : Type u_2} → [Add α] → (α → β) → α → Prop
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.apply_symm_apply : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (p : P₂), e (e.symm p) = p
-- Mathlib.Order.Filter.IsBounded
Filter.isCoboundedUnder_ge_of_eventually_le : ∀ {α : Type u_1} {ι : Type u_4} [inst : Preorder α] (l : Filter ι) [l.NeBot] {f : ι → α} {x : α},
  (∀ᶠ (i : ι) in l, f i ≤ x) → Filter.IsCoboundedUnder (fun x1 x2 => x2 ≤ x1) l f
-- Mathlib.CategoryTheory.Center.Basic
CategoryTheory.CatCenter.smul_iso_hom_eq'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (z : (CategoryTheory.CatCenter C)ˣ) {X Y : C} (f : X ≅ Y)
  {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (z • f).hom h =
    CategoryTheory.CategoryStruct.comp ((↑z).app X) (CategoryTheory.CategoryStruct.comp f.hom h)
-- Mathlib.LinearAlgebra.Ray
/-- The rays given by two nonzero vectors are equal if and only if those vectors
satisfy `SameRay`.  -/
ray_eq_iff : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {v₁ v₂ : M} (hv₁ : v₁ ≠ 0) (hv₂ : v₂ ≠ 0),
  rayOfNeZero R v₁ hv₁ = rayOfNeZero R v₂ hv₂ ↔ SameRay R v₁ v₂
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.refl : ∀ {α : Type u} {L : List (α × Bool)}, FreeGroup.Red L L
-- Mathlib.NumberTheory.Bernoulli
_private.Mathlib.NumberTheory.Bernoulli.0.Bernoulli.not_dvd_den_bernoulli_add_indicator : ∀ {k p : ℕ}, k > 0 → ∀ [Fact (Nat.Prime p)], ¬p ∣ (bernoulli (2 * k) + Bernoulli.vonStaudtIndicator✝ (2 * k) p / ↑p).den
-- Std.Tactic.BVDecide.LRAT.Internal.Convert
_private.Std.Tactic.BVDecide.LRAT.Internal.Convert.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray.folder.match_6.eq_1 : ∀ {n : ℕ} (motive : Option (Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool) → Sort u_1)
  (h_1 : Unit → motive none)
  (h_2 : (map : Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool) → motive (some map)),
  (match none with
    | none => h_1 ()
    | some map => h_2 map) =
    h_1 ()
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.algebra.eq_1 : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddMonoid M],
  AddMonoidAlgebra.algebra =
    { toSMul := AddMonoidAlgebra.smulZeroClass.toSMul,
      algebraMap := AddMonoidAlgebra.singleZeroRingHom.comp (algebraMap R A), commutes' := ⋯, smul_def' := ⋯ }
-- Mathlib.Algebra.Group.Int.Even
Int.not_even_iff : ∀ {n : ℤ}, ¬Even n ↔ n % 2 = 1
-- Lean.Widget.UserWidget
Lean.Widget.instRpcEncodablePanelWidgetInstance : Lean.Server.RpcEncodable Lean.Widget.PanelWidgetInstance
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.erase_empty : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {k : α}, ∅.erase k = ∅
-- Init.Tactics
/-- Argument for the `clear_value` tactic.
 -/
Lean.Parser.Tactic.clearValueArg : Lean.ParserDescr
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
AddSubsemigroup.mem_centralizer_iff : ∀ {M : Type u_1} {S : Set M} [inst : AddSemigroup M] {z : M}, z ∈ AddSubsemigroup.centralizer S ↔ ∀ g ∈ S, g + z = z + g
-- Std.Internal.Do.Order.Instances
Std.Internal.Do.CompleteLattice.instLeftIdentityMeetTop : ∀ {l : Type u_1} [inst : Lean.Order.CompleteLattice l],
  Std.LeftIdentity (fun x1 x2 => Lean.Order.meet x1 x2) Lean.Order.top
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.empty_mul : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] (s : Finset α), ∅ * s = ∅
-- Lean.Elab.DocString
Lean.Doc.DocArg.num.inj : ∀ {val val_1 : Lean.NumLit}, Lean.Doc.DocArg.num val = Lean.Doc.DocArg.num val_1 → val = val_1
-- Init.Data.List.TakeDrop
List.drop_one : ∀ {α : Type u_1} {l : List α}, List.drop 1 l = l.tail
-- Mathlib.Analysis.LocallyConvex.Basic
/-- The interior of a balanced set is balanced if it contains the origin.  -/
Balanced.interior : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {A : Set E}
  [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E], Balanced 𝕜 A → 0 ∈ interior A → Balanced 𝕜 (interior A)
-- Mathlib.NumberTheory.NumberField.Completion.Ramification
/-- The degree of `L` over `K` is equal to the sum of the inertia degrees of the places over `v`.  -/
NumberField.InfinitePlace.sum_inertiaDeg_eq_finrank : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (v : NumberField.InfinitePlace K) [NumberField K] [inst_4 : NumberField L],
  ∑ w ∈ (NumberField.InfinitePlace.placesOver L v).toFinset, v.inertiaDeg w = Module.finrank K L
-- Mathlib.Algebra.GroupWithZero.WithZero
/-- **Alias** of the reverse direction of `WithZero.map'_injective_iff`. -/
WithZero.map'_injective : ∀ {α : Type u_1} {β : Type u_2} [inst : MulOneClass α] [inst_1 : MulOneClass β] {f : α →* β},
  Function.Injective ⇑f → Function.Injective ⇑(WithZero.map' f)
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.Prototile.instCoeOutSet : {G : Type u_1} →
  {X : Type u_2} → [inst : Group G] → [inst_1 : MulAction G X] → CoeOut (DiscreteTiling.Prototile G X) (Set X)
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.SubmersivePresentation.basisDeriv.eq_1 : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ),
  P.basisDeriv = (Pi.basisFun S σ).map P.aevalDifferentialEquiv
-- Mathlib.RingTheory.WittVector.WittPolynomial
/-- Over the ring `ZMod (p^(n+1))`, we produce the `n+1`st Witt polynomial
by expanding the `n`th Witt polynomial by `p`.  -/
wittPolynomial_zmod_self : ∀ (p n : ℕ),
  wittPolynomial p (ZMod (p ^ (n + 1))) (n + 1) = (MvPolynomial.expand p) (wittPolynomial p (ZMod (p ^ (n + 1))) n)
-- Mathlib.Analysis.LocallyConvex.AbsConvex
AbsConvex.absConvexHull_subset_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜] {s t : Set E}, AbsConvex 𝕜 t → ((absConvexHull 𝕜) s ⊆ t ↔ s ⊆ t)
-- Mathlib.Topology.EMetricSpace.Defs
PseudoEMetricSpace.edist_self : ∀ {α : Type u} [self : PseudoEMetricSpace α] (x : α), edist x x = 0
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- Characterization of the sheaf hom on basic opens,
direction ← (next lemma) is used at various places, but → is not used in this file.  -/
AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_iff : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) (r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X)))
  (f :
    (AlgebraicGeometry.Spec.structureSheaf ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))).obj.obj
        (Opposite.op (PrimeSpectrum.basicOpen r)) ⟶
      X.presheaf.obj (Opposite.op (X.toΓSpecMapBasicOpen r))),
  CategoryTheory.CategoryStruct.comp
        (CommRingCat.ofHom
          (algebraMap (↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X)))
            ((AlgebraicGeometry.structureSheafInType ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))
                    ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))).obj.obj
              (Opposite.op (PrimeSpectrum.basicOpen r)))))
        f =
      X.toToΓSpecMapBasicOpen r ↔
    f = X.toΓSpecCApp r
-- Init.Data.BitVec.Lemmas
BitVec.le_refl : ∀ {n : ℕ} (x : BitVec n), x ≤ x
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.postcomp_shiftIso_inv_app : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E] {A : Type u_5}
  [inst_3 : AddMonoid A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : CategoryTheory.HasShift E A]
  (F : CategoryTheory.SingleFunctors C D A) (G : CategoryTheory.Functor D E) [inst_6 : G.CommShift A] (n a a' : A)
  (ha' : n + a = a') (X : C),
  ((F.postcomp G).shiftIso n a a' ha').inv.app X =
    CategoryTheory.CategoryStruct.comp (G.map ((F.shiftIso n a a' ha').inv.app X))
      ((CategoryTheory.Functor.commShiftIso G n).hom.app ((F.functor a').obj X))
-- Mathlib.Algebra.Ring.Action.Invariant
/-- The canonical inclusion from an invariant subring.  -/
IsInvariantSubring.subtypeHom : (M : Type u_1) →
  [inst : Monoid M] →
    {R' : Type u_2} →
      [inst_1 : Ring R'] →
        [inst_2 : MulSemiringAction M R'] → (U : Subring R') → [inst_3 : IsInvariantSubring M U] → ↥U →+*[M] R'
-- Mathlib.Algebra.Module.Submodule.Bilinear
/-- Map a pair of submodules under a bilinear map.

This is the submodule version of `Set.image2`.  -/
Submodule.map₂ : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {P : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid N] →
              [inst_3 : AddCommMonoid P] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module R P] → (M →ₗ[R] N →ₗ[R] P) → Submodule R M → Submodule R N → Submodule R P
-- Mathlib.Algebra.Order.Monoid.Submonoid
/-- A submonoid of an ordered monoid is an ordered monoid.  -/
Submonoid.toIsOrderedMonoid : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedMonoid M] (S : Submonoid M), IsOrderedMonoid ↥S
-- Init.System.ST
/-- Atomically modifies a mutable reference cell by replacing its contents with the result of a function
call.
 -/
ST.Ref.modify : {σ : Type} → {m : Type → Type} → [MonadLiftT (ST σ) m] → {α : Type} → ST.Ref σ α → (α → α) → m Unit
-- Init.Data.UInt.Lemmas
USize.toUInt16_toUInt8 : ∀ (n : USize), n.toUInt8.toUInt16 = n.toUInt16 % 256
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instInhabitedMon : Inhabited Lean.Grind.CommRing.Mon
-- Mathlib.CategoryTheory.Products.Associator
CategoryTheory.prod.prodμ_inverse_map : ∀ (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] (A : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A] {X Y : (A × D) × C × E} (f : X ⟶ Y),
  (CategoryTheory.prod.prodμ C D E A).inverse.map f =
    CategoryTheory.Prod.mkHom (CategoryTheory.Prod.mkHom f.1.1 f.2.1) (CategoryTheory.Prod.mkHom f.1.2 f.2.2)
-- Init.Data.Float.Float32
/-- Obtains the `Float32` whose value is the same as the given `UInt8`.  -/
UInt8.toFloat32 : UInt8 → Float32
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.Hom.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {HP HP' : TopPair.HomologyPretheory C c} (homₚ : (i : ι) → HP.Hₚ i ⟶ HP'.Hₚ i)
  (hom : (i : ι) → HP.H i ⟶ HP'.H i)
  (iso_comm :
    autoParam
      (∀ (i : ι),
        CategoryTheory.CategoryStruct.comp (HP.iso i).hom (TopPair.incl.whiskerLeft (homₚ i)) =
          CategoryTheory.CategoryStruct.comp (hom i) (HP'.iso i).hom)
      TopPair.HomologyPretheory.Hom.iso_comm._autoParam)
  (w :
    autoParam
      (∀ (i j : ι),
        CategoryTheory.CategoryStruct.comp (HP.δ i j) (TopPair.proj₂.whiskerLeft (hom j)) =
          CategoryTheory.CategoryStruct.comp (homₚ i) (HP'.δ i j))
      TopPair.HomologyPretheory.Hom.w._autoParam)
  (homₚ_1 : (i : ι) → HP.Hₚ i ⟶ HP'.Hₚ i) (hom_1 : (i : ι) → HP.H i ⟶ HP'.H i)
  (iso_comm_1 :
    autoParam
      (∀ (i : ι),
        CategoryTheory.CategoryStruct.comp (HP.iso i).hom (TopPair.incl.whiskerLeft (homₚ_1 i)) =
          CategoryTheory.CategoryStruct.comp (hom_1 i) (HP'.iso i).hom)
      TopPair.HomologyPretheory.Hom.iso_comm._autoParam)
  (w_1 :
    autoParam
      (∀ (i j : ι),
        CategoryTheory.CategoryStruct.comp (HP.δ i j) (TopPair.proj₂.whiskerLeft (hom_1 j)) =
          CategoryTheory.CategoryStruct.comp (homₚ_1 i) (HP'.δ i j))
      TopPair.HomologyPretheory.Hom.w._autoParam),
  ({ homₚ := homₚ, hom := hom, iso_comm := iso_comm, w := w } =
      { homₚ := homₚ_1, hom := hom_1, iso_comm := iso_comm_1, w := w_1 }) =
    (homₚ = homₚ_1 ∧ hom = hom_1)
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.toGenerators_comp : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (Q : Algebra.PreSubmersivePresentation S T ι' σ')
  (P : Algebra.PreSubmersivePresentation R S ι σ), (Q.comp P).toGenerators = Q.comp P.toGenerators
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
/-- The pullback along an embedding is (isomorphic to) the preimage.  -/
TopCat.pullbackHomeoPreimage : {X : Type u_1} →
  {Y : Type u_2} →
    {Z : Type u_3} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] →
          [inst_2 : TopologicalSpace Z] →
            (f : X → Z) →
              Continuous f → (g : Y → Z) → Topology.IsEmbedding g → { p // f p.1 = g p.2 } ≃ₜ ↑(f ⁻¹' Set.range g)
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.OplaxTrans.Modification.mk.congr_simp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (app app_1 : (a : B) → η.app a ⟶ θ.app a) (e_app : app = app_1)
  (naturality :
    ∀ {a b : B} (f : a ⟶ b),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b)) (θ.naturality f) =
        CategoryTheory.CategoryStruct.comp (η.naturality f) (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f))),
  { app := app, naturality := naturality } = { app := app_1, naturality := ⋯ }
-- Mathlib.Util.Export
Lean.Export.Entry.name.injEq : ∀ (n n_1 : Lean.Name), (Lean.Export.Entry.name n = Lean.Export.Entry.name n_1) = (n = n_1)
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.FiniteAtFilter.exists_mem_basis : ∀ {α : Type u_1} {ι : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α},
  μ.FiniteAtFilter f → ∀ {p : ι → Prop} {s : ι → Set α}, f.HasBasis p s → ∃ i, p i ∧ μ (s i) < ⊤
-- Aesop.Tree.Data
Aesop.MVarClusterData.mk.injEq : ∀ {Goal Rapp : Type} (parent? : Option (IO.Ref Rapp)) (goals : Array (IO.Ref Goal)) (isIrrelevant : Bool)
  (state : Aesop.NodeState) (parent?_1 : Option (IO.Ref Rapp)) (goals_1 : Array (IO.Ref Goal)) (isIrrelevant_1 : Bool)
  (state_1 : Aesop.NodeState),
  ({ parent? := parent?, goals := goals, isIrrelevant := isIrrelevant, state := state } =
      { parent? := parent?_1, goals := goals_1, isIrrelevant := isIrrelevant_1, state := state_1 }) =
    (parent? = parent?_1 ∧ goals = goals_1 ∧ isIrrelevant = isIrrelevant_1 ∧ state = state_1)
-- Lean.Level
Lean.instReprLevel : Repr Lean.Level
-- Mathlib.Algebra.Group.Prod
Prod.instIsCancelAdd : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] [IsCancelAdd G] [IsCancelAdd H], IsCancelAdd (G × H)
-- Mathlib.LinearAlgebra.Dimension.Basic
/-- The same-universe version of `lift_rank_eq_of_equiv_equiv`.  -/
rank_eq_of_equiv_equiv : ∀ {R : Type u} {R' : Type u'} {M M₁ : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Semiring R'] [inst_4 : AddCommMonoid M₁] [inst_5 : Module R' M₁] (i : R → R') (j : M ≃+ M₁),
  Function.Bijective i → (∀ (r : R) (m : M), j (r • m) = i r • j m) → Module.rank R M = Module.rank R' M₁