mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.InjSurj
/-- A type endowed with `0`, `1`, `+` is an additive group with one,
if it admits a surjective map that preserves `0`, `1`, and `+` to an additive group with one.
See note [reducible non-instances].  -/
Function.Surjective.addGroupWithOne : {R : Type u_1} →
  {S : Type u_2} →
    (f : R → S) →
      Function.Surjective f →
        [inst : Add S] →
          [inst_1 : Zero S] →
            [inst_2 : One S] →
              [inst_3 : Neg S] →
                [inst_4 : Sub S] →
                  [inst_5 : SMul ℕ S] →
                    [inst_6 : SMul ℤ S] →
                      [inst_7 : NatCast S] →
                        [inst_8 : IntCast S] →
                          [inst_9 : AddGroupWithOne R] →
                            f 0 = 0 →
                              f 1 = 1 →
                                (∀ (x y : R), f (x + y) = f x + f y) →
                                  (∀ (x : R), f (-x) = -f x) →
                                    (∀ (x y : R), f (x - y) = f x - f y) →
                                      (∀ (n : ℕ) (x : R), f (n • x) = n • f x) →
                                        (∀ (n : ℤ) (x : R), f (n • x) = n • f x) →
                                          (∀ (n : ℕ), f ↑n = ↑n) → (∀ (n : ℤ), f ↑n = ↑n) → AddGroupWithOne S
-- Init.Meta.Defs
/-- Controls which new mvars are turned in to goals by the `apply` tactic.
- `nonDependentFirst`  mvars that don't depend on other goals appear first in the goal list.
- `nonDependentOnly` only mvars that don't depend on other goals are added to goal list.
- `all` all unassigned mvars are added to the goal list.
 -/
Lean.Meta.Rewrite.NewGoals : Type
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add.0.Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput.cast.match_1.splitter : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig1 : Std.Sat.AIG α} →
        (motive : Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput aig1 → Sort u_1) →
          (val : Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput aig1) →
            ((lhs rhs cin : aig1.Ref) → motive { lhs := lhs, rhs := rhs, cin := cin }) → motive val
-- Mathlib.Data.Set.NAry
Set.image_image2 : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {s : Set α} {t : Set β} (f : α → β → γ) (g : γ → δ),
  g '' Set.image2 f s t = Set.image2 (fun a b => g (f a b)) s t
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.withNonTerminal : {α : Type} → Lean.Elab.Tactic.Try.TryTacticM α → Lean.Elab.Tactic.Try.TryTacticM α
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.inter : ∀ {α : Type u} {s t s' t' : Set α} {l : Filter α}, s =ᶠ[l] t → s' =ᶠ[l] t' → s ∩ s' =ᶠ[l] t ∩ t'
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, (m.erase k).isEmpty = (m.isEmpty || m.size == 1 && m.contains k)
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
Subgroup.op_le_iff : ∀ {G : Type u_2} [inst : Group G] {S₁ : Subgroup G} {S₂ : Subgroup Gᵐᵒᵖ}, S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop
-- Mathlib.Algebra.Ring.Basic
neg_div' : ∀ {R : Type u_1} [inst : DivisionMonoid R] [inst_1 : HasDistribNeg R] (a b : R), -(b / a) = -b / a
-- Init.Data.Array.Attach
Array.pmap_congr_left : ∀ {α : Type u_1} {β : Type u_2} {p q : α → Prop} {f : (a : α) → p a → β} {g : (a : α) → q a → β} (xs : Array α)
  {H₁ : ∀ a ∈ xs, p a} {H₂ : ∀ a ∈ xs, q a},
  (∀ a ∈ xs, ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂) → Array.pmap f xs H₁ = Array.pmap g xs H₂
-- Mathlib.CategoryTheory.Monoidal.Preadditive
/-- A category is `MonoidalPreadditive` if tensoring is additive in both factors.

Note we don't `extend Preadditive C` here, as `Abelian C` already extends it,
and we'll need to have both typeclasses sometimes.
 -/
CategoryTheory.MonoidalPreadditive : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Preadditive C] → [CategoryTheory.MonoidalCategory C] → Prop
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Negating the first vector produces the same angle as negating the second vector.  -/
Orientation.oangle_neg_left_eq_neg_right : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V), o.oangle (-x) y = o.oangle x (-y)
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.LambdaTheoremArgs.comp.inj : ∀ {fArgId gArgId fArgId_1 gArgId_1 : ℕ},
  Mathlib.Meta.FunProp.LambdaTheoremArgs.comp fArgId gArgId =
      Mathlib.Meta.FunProp.LambdaTheoremArgs.comp fArgId_1 gArgId_1 →
    fArgId = fArgId_1 ∧ gArgId = gArgId_1
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.Hom.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            {A : C} →
              [inst_4 : CategoryTheory.AddMonObj A] →
                {M N : CategoryTheory.AddMod D A} →
                  (hom : M.X ⟶ N.X) → [isAddModHom : CategoryTheory.IsAddModHom A hom] → M.Hom N
-- Mathlib.Data.Nat.Factorization.Basic
Nat.prod_pow_prime_padicValNat : ∀ (n : ℕ), n ≠ 0 → ∀ (m : ℕ), n < m → ∏ p ∈ Finset.range m with Nat.Prime p, p ^ padicValNat p n = n
-- Mathlib.Analysis.Normed.Group.Continuity
tendsto_iff_enorm_div_tendsto_zero : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedCommGroup E] {f : α → E} {a : Filter α} {b : E},
  Filter.Tendsto f a (nhds b) ↔ Filter.Tendsto (fun e => ‖f e / b‖ₑ) a (nhds 0)
-- Lean.Meta.Tactic.Simp.Main
/-- We use `withNewLemmas` whenever updating the local context.
 -/
Lean.Meta.Simp.withNewLemmas : {α : Type} → Array Lean.Expr → Lean.Meta.SimpM α → Lean.Meta.SimpM α
-- Mathlib.Topology.Algebra.MulAction
ContinuousSMul.induced : ∀ {R : Type u_5} {α : Type u_6} {β : Type u_7} {F : Type u_8} [inst : FunLike F α β] [inst_1 : Semiring R]
  [inst_2 : AddCommMonoid α] [inst_3 : AddCommMonoid β] [inst_4 : Module R α] [inst_5 : Module R β]
  [inst_6 : TopologicalSpace R] [LinearMapClass F R α β] [tβ : TopologicalSpace β] [ContinuousSMul R β] (f : F),
  ContinuousSMul R α
-- Mathlib.Analysis.Analytic.ChangeOrigin
/-- If a function admits a power series expansion `p` within a set `s` on a ball `B (x, r)`, then
it also admits a power series on any subball of this ball (even with a different center provided
it belongs to `s`), given by `p.changeOrigin`.  -/
HasFPowerSeriesWithinOnBall.changeOrigin : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x y : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r →
    ‖y‖ₑ < r → x + y ∈ insert x s → HasFPowerSeriesWithinOnBall f (p.changeOrigin y) s (x + y) (r - ‖y‖ₑ)
-- Mathlib.LinearAlgebra.Ray
/-- Two vectors are in the same ray, or the first is in the same ray as the negation of the
second, if and only if they are not linearly independent.  -/
sameRay_or_sameRay_neg_iff_not_linearIndependent : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [Module.IsTorsionFree R M] {x y : M},
  SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.symm_apply_apply : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S) (x : R),
  e.symm (e x) = x
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.ext_ring_iff : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] [Finite ι] [inst_5 : TopologicalSpace R] {f g : R [⋀^ι]→L[R] M},
  f = g ↔ (f fun x => 1) = g fun x => 1
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.isProjectiveMeasureFamily_partialTraj : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1)))
  [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {a : ℕ} (x₀ : (i : ↥(Finset.Iic a)) → X ↑i),
  MeasureTheory.IsProjectiveMeasureFamily
    (MeasureTheory.inducedFamily fun b => (ProbabilityTheory.Kernel.partialTraj κ a b) x₀)
-- Aesop.Rule.Forward
Aesop.ForwardRulePriority.normSafe.inj : ∀ {n n_1 : ℤ}, Aesop.ForwardRulePriority.normSafe n = Aesop.ForwardRulePriority.normSafe n_1 → n = n_1
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.binaryBiproductTriangle_distinguished : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C] (X₁ X₂ : C),
  CategoryTheory.Pretriangulated.binaryBiproductTriangle X₁ X₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_eq_getKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {a : α} {h : a ∈ t}, t.getKey a h = t.getKey! a
-- Mathlib.Topology.Basic
isOpen_biUnion : ∀ {X : Type u} {α : Type u_1} [inst : TopologicalSpace X] {s : Set α} {f : α → Set X},
  (∀ i ∈ s, IsOpen (f i)) → IsOpen (⋃ i ∈ s, f i)
-- Init.Control.Lawful.Instances
_private.Init.Control.Lawful.Instances.0.Option.getD.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (opt : Option α) → ((x : α) → motive (some x)) → (Unit → motive none) → motive opt
-- Mathlib.Topology.DiscreteSubset
/-- In any topological space, the open sets with discrete complement form a filter,
defined as the supremum of all punctured neighborhoods.

See `Filter.mem_codiscrete'` for the equivalence.  -/
Filter.codiscrete : (X : Type u_3) → [TopologicalSpace X] → Filter X
-- Batteries.Data.String.Lemmas
String.split_of_valid : ∀ (s : String) (p : Char → Bool), s.splitToList p = List.map String.ofList (List.splitOnP p s.toList)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The `v`-adic absolute value of `r / s : K` is the absolute value of `r` divided by the absolute
value of `s`.  -/
IsDedekindDomain.HeightOneSpectrum.adicAbv_of_mk' : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) {b : NNReal}
  (hb : 1 < b) (r : R) {s : ↥(nonZeroDivisors R)},
  (v.adicAbv hb) (IsLocalization.mk' K r s) = (v.intAdicAbv hb) r / (v.intAdicAbv hb) ↑s
-- Mathlib.Algebra.Category.AlgCat.Basic
/-- A ring isomorphism induces an equivalence of categories of algebras.  -/
AlgCat.restrictScalarsEquivalenceOfRingEquiv : {R : Type u_1} → {S : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing S] → R ≃+* S → (AlgCat S ≌ AlgCat R)
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.ext : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : DistribMulAction M A] {B : Type u_5} [inst_4 : AddMonoid B] [inst_5 : DistribMulAction N B]
  {f g : A →ₑ+[φ] B}, (∀ (x : A), f x = g x) → f = g
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.mono_iff_stalk_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {FC : C → C → Type u_1} {CC : C → Type v} [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
  [instCC : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C]
  [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms]
  {F G : TopCat.Sheaf C X} (f : F ⟶ G),
  CategoryTheory.Mono f ↔ ∀ (x : ↑X), CategoryTheory.Mono ((TopCat.Presheaf.stalkFunctor C x).map f.hom)
-- Mathlib.LinearAlgebra.Orientation
/-- The orientation given by a basis derived using `units_smul`, in terms of the product of those
units.  -/
Module.Basis.orientation_unitsSMul : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_4} [inst_5 : Fintype ι] [inst_6 : DecidableEq ι]
  (e : Module.Basis ι R M) (w : ι → Rˣ), (e.unitsSMul w).orientation = (∏ i, w i)⁻¹ • e.orientation
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.hom_ofHom : ∀ {M N : Type u} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N), MagmaCat.Hom.hom (MagmaCat.ofHom f) = f
-- Mathlib.Condensed.Discrete.LocallyConstant
CompHausLike.LocallyConstant.counitAppApp.eq_1 : ∀ {P : TopCat → Prop} [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)]
  [inst_1 : CompHausLike.HasProp P PUnit.{u + 1}] (S : CompHausLike P)
  (Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w)))
  [inst_2 : CategoryTheory.Limits.PreservesFiniteProducts Y] [inst_3 : CompHausLike.HasExplicitFiniteCoproducts P],
  CompHausLike.LocallyConstant.counitAppApp S Y =
    TypeCat.ofHom fun r =>
      (CategoryTheory.ConcreteCategory.hom
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.inv
              (CompHausLike.sigmaComparison Y fun a => ↑(CompHausLike.LocallyConstant.fiber r a).toTop))
            (Y.mapIso (CompHausLike.LocallyConstant.sigmaIso r).op).inv))
        (CompHausLike.LocallyConstant.counitAppAppImage r)
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.map_comp_includeRight : ∀ {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  [inst_7 : Semiring D] [inst_8 : Algebra R D] (f : A →ₐ[R] C) (g : B →ₐ[R] D),
  (Algebra.TensorProduct.map f g).comp Algebra.TensorProduct.includeRight = Algebra.TensorProduct.includeRight.comp g
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.equivYoneda_inv_app_hom_apply : ∀ (S : CategoryTheory.Functor Type uᵒᵖ (Type u))
  (hs : CategoryTheory.Presheaf.IsSheaf CategoryTheory.typesGrothendieckTopology S) (X : Type uᵒᵖ)
  (x : Opposite.unop X ⟶ S.obj (Opposite.op PUnit.{u + 1})),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.equivYoneda S hs).inv.app X)) x =
    (CategoryTheory.evalEquiv S hs (Opposite.unop X)).symm x
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- The characteristic maps are continuous when restricting to `closedBall 0 1`.  -/
Topology.RelCWComplex.continuousOn : ∀ {X : Type u} {inst : TopologicalSpace X} {C : Set X} {D : outParam (Set X)} [self : Topology.RelCWComplex C D] (n : ℕ)
  (i : Topology.RelCWComplex.cell C n), ContinuousOn (↑(Topology.RelCWComplex.map n i)) (Metric.closedBall 0 1)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Class
Std.Tactic.BVDecide.LRAT.Internal.Formula.ofArray : {α : outParam (Type u)} →
  {β : outParam (Type v)} →
    {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} →
      {σ : Type w} →
        {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} →
          [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] → Array (Option β) → σ
-- Init.Data.SInt.Lemmas
ISize.ofInt_tdiv : ∀ {a b : ℤ},
  ISize.minValue.toInt ≤ a →
    a ≤ ISize.maxValue.toInt →
      ISize.minValue.toInt ≤ b → b ≤ ISize.maxValue.toInt → ISize.ofInt (a.tdiv b) = ISize.ofInt a / ISize.ofInt b
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor_obj_right_as : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T × T)
  (Y : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.diag T) X),
  ((CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor X).obj Y).right.as = PUnit.unit
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.coe_symm_trans : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {E : Type u_5} {E₂ : Type u_6} {E₃ : Type u_7} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {σ₁₃ : R →+* R₃} {σ₃₁ : R₃ →+* R}
  {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [inst_3 : RingHomInvPair σ₁₂ σ₂₁] [inst_4 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_5 : RingHomInvPair σ₁₃ σ₃₁] [inst_6 : RingHomInvPair σ₃₁ σ₁₃] [inst_7 : RingHomInvPair σ₂₃ σ₃₂]
  [inst_8 : RingHomInvPair σ₃₂ σ₂₃] [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_10 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
  [inst_11 : SeminormedAddCommGroup E] [inst_12 : SeminormedAddCommGroup E₂] [inst_13 : SeminormedAddCommGroup E₃]
  [inst_14 : Module R E] [inst_15 : Module R₂ E₂] [inst_16 : Module R₃ E₃] (e₁ : E ≃ₛₗᵢ[σ₁₂] E₂) (e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃),
  ⇑(e₁.trans e₂).symm = ⇑e₁.symm ∘ ⇑e₂.symm
-- Init.Data.Float.Model.Float
/-- Converts a `Float.Model` to an `Int32`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float.Model.toInt32 : Float.Model → Int32
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.range_map_mono : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {M₃ : Type u_13}
  {N₂ : Type u_14} {N₃ : Type u_15} [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid M₂]
  [inst_4 : AddCommMonoid N₂] [inst_5 : AddCommMonoid M₃] [inst_6 : AddCommMonoid N₃] [inst_7 : Module R M]
  [inst_8 : Module R N] [inst_9 : Module R M₂] [inst_10 : Module R M₃] [inst_11 : Module R N₂] [inst_12 : Module R N₃]
  {a : M →ₗ[R] M₂} {b : M₃ →ₗ[R] M₂} {c : N →ₗ[R] N₂} {d : N₃ →ₗ[R] N₂},
  a.range ≤ b.range → c.range ≤ d.range → (TensorProduct.map a c).range ≤ (TensorProduct.map b d).range
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsIsometricVAdd.opposite_of_comm : ∀ (M : Type u) (X : Type w) [inst : PseudoEMetricSpace X] [inst_1 : VAdd M X] [inst_2 : VAdd Mᵃᵒᵖ X] [IsCentralVAdd M X]
  [IsIsometricVAdd M X], IsIsometricVAdd Mᵃᵒᵖ X
-- Init.Data.UInt.Lemmas
UInt16.toUInt32_ofNatTruncate_of_lt : ∀ {n : ℕ} (hn : n < UInt16.size), (UInt16.ofNatClamp n).toUInt32 = UInt32.ofNatLT n ⋯
-- Mathlib.Algebra.Ring.CentroidHom
/-- The tautological action by `CentroidHom α` on `α`.

This generalizes `Function.End.applyMulAction`.  -/
CentroidHom.applyModule : {α : Type u_5} → [inst : NonUnitalNonAssocSemiring α] → Module (CentroidHom α) α
-- Mathlib.Order.Hom.Basic
OrderIso.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] {f g : α ≃o β}, ⇑f = ⇑g → f = g
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- Eta-expanded form of `MDifferentiableOn.smul` -/
MDifferentiableOn.fun_smul : ∀ {𝕜 : 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] {s : Set M} {V : Type u_18} [inst_6 : NormedAddCommGroup V]
  [inst_7 : NormedSpace 𝕜 V] {f : M → 𝕜} {g : M → V}, MDiff[s] f → MDiff[s] g → MDiff[s] fun i => f i • g i
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat_rat : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → ℚ → ℝ}
  (hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν) (a : α) (q : ℚ) {s : Set β},
  MeasurableSet s →
    ∫ (b : β) in s, ↑(ProbabilityTheory.stieltjesOfMeasurableRat f ⋯ (a, b)) ↑q ∂ν a = (κ a).real (s ×ˢ Set.Iic ↑q)
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.isOpenQuotientMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  IsOpenQuotientMap ⇑h
-- Mathlib.Topology.Order.Basic
SuccOrder.hasBasis_nhds_Ioc : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [SuccOrder α] {a : α}
  [NoMinOrder α], (nhds a).HasBasis (fun x => x < a) fun x => Set.Ioc x a
-- Mathlib.Data.List.Intervals
List.Ico.isChain_succ : ∀ (n m : ℕ), List.IsChain (fun a b => b = a.succ) (List.Ico n m)
-- Init.Data.List.Basic
List.beq.eq_2 : ∀ {α : Type u} [inst : BEq α] (a : α) (as : List α) (b : α) (bs : List α),
  (a :: as).beq (b :: bs) = (a == b && as.beq bs)
-- Mathlib.Testing.Plausible.Functions
Plausible.TotalFunction.apply.congr_simp : ∀ {α : Type u} {β : Type v} {inst : DecidableEq α} [inst_1 : DecidableEq α] (a a_1 : Plausible.TotalFunction α β),
  a = a_1 → ∀ (a_2 a_3 : α), a_2 = a_3 → a.apply a_2 = a_1.apply a_3
-- Mathlib.RingTheory.Ideal.Prod
Ideal.span_prod_le : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {s : Set R} {t : Set S},
  Ideal.span (s ×ˢ t) ≤ (Ideal.span s).prod (Ideal.span t)
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.finiteDimensional : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] [Finite G] [IsGaloisGroup G K L], FiniteDimensional K L
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- As for coproducts, any functor between categories with biproducts gives rise to a morphism
`⨁ (F.obj ∘ f) ⟶ F.obj (⨁ f)`  -/
CategoryTheory.Functor.biproductComparison' : {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] →
            {J : Type w₁} →
              (F : CategoryTheory.Functor C D) →
                (f : J → C) →
                  [inst_4 : CategoryTheory.Limits.HasBiproduct f] →
                    [inst_5 : CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)] → ⨁ F.obj ∘ f ⟶ F.obj (⨁ f)
-- Mathlib.Algebra.Group.End
Equiv.pow_mulRight : ∀ {α : Type u_4} [inst : Group α] (a : α) (n : ℕ), Equiv.mulRight a ^ n = Equiv.mulRight (a ^ n)
-- Mathlib.LinearAlgebra.Multilinear.DFinsupp
MultilinearMap.fromDFinsuppEquiv_apply : ∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} [inst : DecidableEq ι]
  [inst_1 : Fintype ι] [inst_2 : CommSemiring R] [inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)]
  [inst_4 : (i : ι) → (k : κ i) → Module R (M i k)] {N : Type u_1} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  [inst_7 : (i : ι) → DecidableEq (κ i)] [inst_8 : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)]
  (f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) N) (x : (i : ι) → Π₀ (j : κ i), M i j),
  ((MultilinearMap.fromDFinsuppEquiv κ R) f) x =
    ∑ p ∈ Fintype.piFinset fun i => (x i).support, (f p) fun i => (x i) (p i)
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
mem_completeIntegralClosure : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S},
  x ∈ completeIntegralClosure R S ↔ IsAlmostIntegral R x
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get!_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  [inst_1 : Inhabited β], k ∉ t₁ → (t₁ ∪ t₂).get! k = t₂.get! k
-- Mathlib.Algebra.Notation.Defs
ite_div : ∀ {α : Type u_2} (P : Prop) [inst : Decidable P] [inst_1 : Div α] (a b c : α),
  (if P then a else b) / c = if P then a / c else b / c
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePushoutShape.category : {J : Type w} → CategoryTheory.SmallCategory (CategoryTheory.Limits.WidePushoutShape J)