mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.KrullDimension.Module
/-- The krull dimension of module, defined as `krullDim` of its support.  -/
Module.supportDim : (R : Type u_1) → [inst : CommRing R] → (M : Type u_2) → [inst_1 : AddCommGroup M] → [Module R M] → WithBot ℕ∞
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.one_def : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → One (G i)] [∀ (i j : ι) (h : i ≤ j), OneHomClass (T h) (G i) (G j)] (i : ι), 1 = ⟦⟨i, 1⟩⟧
-- Mathlib.Data.Setoid.Partition
/-- A partition of `α` does not contain the empty set.  -/
Setoid.nonempty_of_mem_partition : ∀ {α : Type u_1} {c : Set (Set α)}, Setoid.IsPartition c → ∀ {s : Set α}, s ∈ c → s.Nonempty
-- Mathlib.Algebra.Group.Ext
CancelCommMonoid.toCommMonoid_injective : ∀ {M : Type u}, Function.Injective (@CancelCommMonoid.toCommMonoid M)
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.instCoeGrpCat : Coe CommGrpCat GrpCat
-- Plausible.Testable
Plausible.NamedBinder : String → Prop → Prop
-- Mathlib.Topology.Algebra.NonUnitalStarAlgebra
NonUnitalStarAlgebra.elemental.instNonUnitalCommRingSubtypeMemNonUnitalStarSubalgebraOfT2SpaceOfIsStarNormal : {R : Type u_3} →
  {A : Type u_4} →
    [inst : CommRing R] →
      [inst_1 : StarRing R] →
        [inst_2 : NonUnitalRing A] →
          [inst_3 : StarRing A] →
            [inst_4 : Module R A] →
              [inst_5 : IsScalarTower R A A] →
                [inst_6 : SMulCommClass R A A] →
                  [inst_7 : StarModule R A] →
                    [inst_8 : TopologicalSpace A] →
                      [inst_9 : IsSemitopologicalRing A] →
                        [inst_10 : ContinuousConstSMul R A] →
                          [inst_11 : ContinuousStar A] →
                            [T2Space A] →
                              {x : A} → [IsStarNormal x] → NonUnitalCommRing ↥(NonUnitalStarAlgebra.elemental R x)
-- Mathlib.Algebra.Star.Unitary
Unitary.instInvolutiveStarSubtypeMemSubmonoidUnitary : {R : Type u_1} → [inst : Monoid R] → [inst_1 : StarMul R] → InvolutiveStar ↥(unitary R)
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instStarModule : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R]
  [inst_3 : CommSemiring R] [inst_4 : IsTopologicalSemiring R] [inst_5 : StarRing R] {M : Type u_3}
  [inst_6 : SMulZeroClass M R] [inst_7 : ContinuousConstSMul M R] [inst_8 : Star M] [StarModule M R]
  [inst_10 : ContinuousStar R], StarModule M (ContinuousMapZero X R)
-- Mathlib.Analysis.Convex.Segment
Pi.image_update_openSegment : ∀ {𝕜 : Type u_1} {ι : Type u_5} {M : ι → Type u_6} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : (i : ι) → AddCommMonoid (M i)] [inst_3 : (i : ι) → Module 𝕜 (M i)] [inst_4 : DecidableEq ι] (i : ι)
  (x₁ x₂ : M i) (y : (i : ι) → M i),
  Function.update y i '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (Function.update y i x₁) (Function.update y i x₂)
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.subst_smul : ∀ {A : Type u_1} [inst : CommRing A] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra A R] {τ : Type u_3}
  {S : Type u_4} [inst_3 : CommRing S] [inst_4 : Algebra R S] {a : MvPowerSeries τ S} [inst_5 : Algebra A S]
  [IsScalarTower A R S],
  PowerSeries.HasSubst a → ∀ (r : A) (f : PowerSeries R), PowerSeries.subst a (r • f) = r • PowerSeries.subst a f
-- Std.Data.DTreeMap.Internal.Lemmas
_private.Std.Data.DTreeMap.Internal.Lemmas.0.Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew?.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.SetTheory.Cardinal.Ordinal
Ordinal.card_opow_le_of_omega0_le_right : ∀ (a : Ordinal.{u_1}) {b : Ordinal.{u_1}}, Ordinal.omega0 ≤ b → (a ^ b).card ≤ max a.card b.card
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
CategoryTheory.EffectiveEpiFamily.hom_ext : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {B W : C} {α : Type u_2} (X : α → C)
  (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π] (m₁ m₂ : B ⟶ W),
  (∀ (a : α), CategoryTheory.CategoryStruct.comp (π a) m₁ = CategoryTheory.CategoryStruct.comp (π a) m₂) → m₁ = m₂
-- Mathlib.Data.Quot
/-- `Quotient.mk'` is a surjective function.  -/
Quotient.mk'_surjective : ∀ {α : Sort u_1} [s : Setoid α], Function.Surjective Quotient.mk'
-- Mathlib.Algebra.Category.Grp.Adjunctions
/-- The free functor `Type u ⥤ AddCommGroup` sending a type `X` to the
free abelian group with generators `x : X`.
 -/
AddCommGrpCat.free : CategoryTheory.Functor (Type u) AddCommGrpCat
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- **Alias** of the reverse direction of `hasFDerivWithinAt_sub_const_iff`. -/
HasFDerivWithinAt.sub_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} {s : Set E} (c : F), HasFDerivWithinAt f f' s x → HasFDerivWithinAt (fun x => f x - c) f' s x
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inv_range : ∀ {α : Type u_2} [inst : InvolutiveInv α] {ι : Sort u_5} {f : ι → α}, (Set.range f)⁻¹ = Set.range fun i => (f i)⁻¹
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.free_bot : ∀ {α : Type u_4} {β : Type u_5} {A : SimpleGraph α}, A ≠ ⊥ → A.Free ⊥
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.inv_iff : ∀ {R : Type u_1} [inst : Group R] [inst_1 : StarMul R] (x : R), IsSelfAdjoint x⁻¹ ↔ IsSelfAdjoint x
-- Mathlib.Data.Seq.Computation
Computation.liftRel_pure_right : ∀ {α : Type u} {β : Type v} (R : α → β → Prop) (ca : Computation α) (b : β),
  Computation.LiftRel R ca (Computation.pure b) ↔ ∃ a ∈ ca, R a b
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.instSMulSubtypeMemTorsion' : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          (S : Type u_3) →
            [inst_3 : CommMonoid S] →
              [inst_4 : DistribMulAction S M] → [inst_5 : SMulCommClass S R M] → SMul S ↥(Submodule.torsion' R M S)
-- Init.Data.String.OrderInstances
String.Pos.Raw.instAntisymmLe : Std.Antisymm fun x1 x2 => x1 ≤ x2
-- Mathlib.RepresentationTheory.Invariants
/-- Given a normal subgroup `S ≤ G`, a `G`-representation `ρ` induces a `G ⧸ S`-representation on
the invariants of `ρ|_S`.  -/
Representation.quotientToInvariants : {k : Type u_1} →
  {G : Type u_2} →
    [inst : CommRing k] →
      [inst_1 : Group G] →
        {V : Type u_5} →
          [inst_2 : AddCommGroup V] →
            [inst_3 : Module k V] →
              (ρ : Representation k G V) →
                (S : Subgroup G) →
                  [inst_4 : S.Normal] →
                    Representation k (G ⧸ S) ↥(Representation.invariants (MonoidHom.comp ρ S.subtype))
-- Mathlib.Tactic.ProxyType
/-- Helper function for `proxy_equiv% type : expectedType` elaborators.

Elaborate `type` and get its `InductiveVal`. Uses the `expectedType`, where the
expected type should be of the form `_ ≃ type`.  -/
Mathlib.ProxyType.elabProxyEquiv : Lean.Term → Option Lean.Expr → Lean.Elab.TermElabM (Lean.Expr × Lean.InductiveVal)
-- Mathlib.Data.Sym.Sym2
/-- This is the relation capturing the notion of pairs equivalent up to permutations.  -/
Sym2.Rel : (α : Type u) → α × α → α × α → Prop
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesOnBall.unique : ∀ {𝕜 : 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] {f g : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal},
  HasFPowerSeriesOnBall f p x r → HasFPowerSeriesOnBall g p x r → Set.EqOn f g (Metric.eball x r)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.dropLast_cons_nil : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v),
  (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil).dropLast = SimpleGraph.Walk.nil
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.coe_toAddSubgroup : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] {module_M : Module R M} (p : Submodule R M),
  ↑p.toAddSubgroup = ↑p
-- Mathlib.Algebra.Polynomial.Module.Basic
/-- The image of a polynomial under a linear map.  -/
PolynomialModule.map : {R : Type u_2} →
  {M : Type u_3} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (R' : Type u_6) →
            {M' : Type u_7} →
              [inst_3 : CommRing R'] →
                [inst_4 : AddCommGroup M'] →
                  [inst_5 : Module R' M'] →
                    [inst_6 : Module R M'] → (M →ₗ[R] M') → PolynomialModule R M →ₗ[R] PolynomialModule R' M'
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.single_zero_comm : ∀ {R : Type u_1} {M : Type u_4} [inst : CommSemiring R] [inst_1 : AddZeroClass M] (r : R) (f : AddMonoidAlgebra R M),
  AddMonoidAlgebra.single 0 r * f = f * AddMonoidAlgebra.single 0 r
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.contract_eq_delete_of_subset_coloops : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, X ⊆ M.coloops → M.contract X = M.delete X
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.φ_ne_zero : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)}, E ≠ ⊥ → RatFunc.Luroth.φ✝ E ≠ 0
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- Any comparison whose history is not minimal is redundant,
and need not be included in the new set of comparisons.
`elimedGE : ℕ` is a natural number such that all variables with index ≥ `elimedGE` have been
removed from the system.

This test is an overapproximation to minimality. It gives necessary but not sufficient conditions.
If the history of `c` is minimal, then `c.maybeMinimal` is true,
but `c.maybeMinimal` may also be true for some `c` with non-minimal history.
Thus, if `c.maybeMinimal` is false, `c` is known not to be minimal and must be redundant.
See https://doi.org/10.1016/B978-0-444-88771-9.50019-2 (Theorem 13).
The condition described there considers only implicitly eliminated variables that have been
officially eliminated from the system. This is not the case for every implicitly eliminated
variable. Consider eliminating `z` from `{x + y + z < 0, x - y - z < 0}`. The result is the set
`{2*x < 0}`; `y` is implicitly but not officially eliminated.

This implementation of Fourier-Motzkin elimination processes variables in decreasing order of
indices. Immediately after a step that eliminates variable `k`, variable `k'` has been eliminated
iff `k' ≥ k`. Thus we can compute the intersection of officially and implicitly eliminated variables
by taking the set of implicitly eliminated variables with indices ≥ `elimedGE`.
 -/
Mathlib.Tactic.Linarith.PComp.maybeMinimal : Mathlib.Tactic.Linarith.PComp → ℕ → Bool
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
ContinuousLinearMap.IsFredholm.finite_ker : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E]
  [inst_6 : TopologicalSpace F] {u : E →L[𝕜] F}, u.IsFredholm → FiniteDimensional 𝕜 ↥(↑u).ker
-- Mathlib.Algebra.Star.Conjneg
support_conjneg : ∀ {G : Type u_2} {R : Type u_3} [inst : AddGroup G] [inst_1 : CommSemiring R] [inst_2 : StarRing R] (f : G → R),
  Function.support (conjneg f) = -Function.support f
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.Core.mk.inj : ∀ {α : Type u} {uniformity : Filter (α × α)} {refl : Filter.principal SetRel.id ≤ uniformity}
  {symm : Filter.Tendsto Prod.swap uniformity uniformity}
  {comp : (uniformity.lift' fun s => SetRel.comp s s) ≤ uniformity} {uniformity_1 : Filter (α × α)}
  {refl_1 : Filter.principal SetRel.id ≤ uniformity_1} {symm_1 : Filter.Tendsto Prod.swap uniformity_1 uniformity_1}
  {comp_1 : (uniformity_1.lift' fun s => SetRel.comp s s) ≤ uniformity_1},
  { uniformity := uniformity, refl := refl, symm := symm, comp := comp } =
      { uniformity := uniformity_1, refl := refl_1, symm := symm_1, comp := comp_1 } →
    uniformity = uniformity_1
-- Plausible.Shrinkable
Plausible.Bool.shrinkable : Plausible.Shrinkable Bool
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.forIn'_congr : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerableLE α] [inst_4 : Std.Rxc.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [inst_6 : Monad m] {γ : Type u} {init init' : γ}
  {r r' : Std.Rcc α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} {f' : (a : α) → a ∈ r' → γ → m (ForInStep γ)}
  (hr : r = r'),
  init = init' → (∀ (a : α) (m_1 : a ∈ r') (b : γ), f a ⋯ b = f' a m_1 b) → forIn' r init f = forIn' r' init' f'
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.ext_get?_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : LawfulBEq α] {m₁ m₂ : Std.ExtDHashMap α β},
  m₁ = m₂ ↔ ∀ (k : α), m₁.get? k = m₂.get? k
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
ProfiniteGrp.diagram_map : ∀ (P : ProfiniteGrp.{u}) {X Y : OpenNormalSubgroup ↑P.toProfinite.toTop} (f : X ⟶ Y),
  P.diagram.map f = (CategoryTheory.forget₂ FiniteGrp.{u} ProfiniteGrp.{u}).map (P.toFiniteQuotientFunctor.map f)
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.instNoncompactSpace : ∀ {α : Type u_1} [inst : TopologicalSpace α] [NoncompactSpace α], NoncompactSpace (TopologicalSpace.NonemptyCompacts α)
-- Mathlib.Order.BooleanAlgebra.Basic
Pi.instBooleanAlgebra : {ι : Type u} → {α : ι → Type v} → [(i : ι) → BooleanAlgebra (α i)] → BooleanAlgebra ((i : ι) → α i)
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.IsAdjMatrix.zero_or_one : ∀ {α : Type u_1} {V : Type u_2} [inst : Zero α] [inst_1 : One α] {A : Matrix V V α},
  A.IsAdjMatrix → ∀ (i j : V), A i j = 0 ∨ A i j = 1
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.mem_bot : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] {x : A}, x ∈ ⊥ ↔ x = 0
-- Mathlib.CategoryTheory.Monad.Algebra
/-- The forgetful functor from the Eilenberg-Moore category, forgetting the algebraic structure.  -/
CategoryTheory.Monad.forget : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → (T : CategoryTheory.Monad C) → CategoryTheory.Functor T.Algebra C
-- Mathlib.Algebra.Category.ModuleCat.Colimits
ModuleCat.forget₂PreservesColimitsOfShape : ∀ (R : Type w) [inst : Ring R] (J : Type u) [inst_1 : CategoryTheory.Category.{v, u} J]
  [CategoryTheory.Limits.HasColimitsOfShape J AddCommGrpCat],
  CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)
-- Mathlib.Topology.Order.LowerUpperTopology
/-- The lower closure of a finite set is closed in the upper topology.  -/
Topology.IsUpper.isClosed_lowerClosure : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsUpper α] {s : Set α},
  s.Finite → IsClosed ↑(lowerClosure s)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.map_inf : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (f : A →ₐ[R] B),
  Function.Injective ⇑f → ∀ (S T : Subalgebra R A), Subalgebra.map f (S ⊓ T) = Subalgebra.map f S ⊓ Subalgebra.map f T
-- Mathlib.SetTheory.Ordinal.Basic
/-- The underlying relation of the order.  -/
WellOrder.r : (self : WellOrder) → self.α → self.α → Prop
-- Init.Data.SInt.Lemmas
Int64.ofNat_le_iff_le : ∀ {a b : ℕ}, a < 2 ^ 63 → b < 2 ^ 63 → (Int64.ofNat a ≤ Int64.ofNat b ↔ a ≤ b)
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.coe_injective : ∀ {𝕜 : 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} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G],
  Function.Injective DFunLike.coe
-- Mathlib.Topology.Gluing
/-- A family of gluing data consists of
1. An index type `J`
2. An object `U i` for each `i : J`.
3. An object `V i j` for each `i j : J`.
  (Note that this is `J × J → TopCat` rather than `J → J → TopCat` to connect to the
  limits library easier.)
4. An open embedding `f i j : V i j ⟶ U i` for each `i j : ι`.
5. A transition map `t i j : V i j ⟶ V j i` for each `i j : ι`.

such that
6. `f i i` is an isomorphism.
7. `t i i` is the identity.
8. `V i j ×[U i] V i k ⟶ V i j ⟶ V j i` factors through `V j k ×[U j] V j i ⟶ V j i` via some
    `t' : V i j ×[U i] V i k ⟶ V j k ×[U j] V j i`.
    (This merely means that `V i j ∩ V i k ⊆ t i j ⁻¹' (V j i ∩ V j k)`.)
9. `t' i j k ≫ t' j k i ≫ t' k i j = 𝟙 _`.

We can then glue the topological spaces `U i` together by identifying `V i j` with `V j i`, such
that the `U i`'s are open subspaces of the glued space.

Most of the times it would be easier to use the constructor `TopCat.GlueData.mk'` where the
conditions are stated in a less categorical way.
 -/
TopCat.GlueData : Type (u_1 + 1)
-- Mathlib.Order.RelIso.Basic
RelEmbedding.sumLexInl_apply : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) (val : α),
  (RelEmbedding.sumLexInl r s) val = Sum.inl val
-- Mathlib.Order.UpperLower.Closure
IsLowerSet.lowerClosure : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, IsLowerSet s → ↑(lowerClosure s) = s
-- Mathlib.Analysis.Complex.Basic
/-- A shortcut instance to ensure computability; otherwise we get the noncomputable instance
`Complex.instNormedField.toNormedModule.toModule`.  -/
Complex.instModuleSelf : Module ℂ ℂ
-- Mathlib.GroupTheory.Coxeter.Basic
/-- The product of the simple reflections of `W` corresponding to the indices in `ω`.  -/
CoxeterSystem.wordProd : {B : Type u_1} → {W : Type u_3} → [inst : Group W] → {M : CoxeterMatrix B} → CoxeterSystem M W → List B → W
-- Mathlib.Algebra.Group.TypeTags.Basic
Additive.addRightCancelMonoid : {α : Type u} → [RightCancelMonoid α] → AddRightCancelMonoid (Additive α)
-- Mathlib.Data.Set.Pairwise.Basic
pairwise_on_bool : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Symm r] {a b : α},
  Pairwise (Function.onFun r fun c => bif c then a else b) ↔ r a b
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
contMDiffWithinAt_prod_module_iff : ∀ {𝕜 : 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] {F₁ : Type u_14} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_15} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂] {s : Set M}
  {x : M} {n : WithTop ℕ∞} (f : M → F₁ × F₂),
  ContMDiffWithinAt I (modelWithCornersSelf 𝕜 (F₁ × F₂)) n f s x ↔
    ContMDiffWithinAt I (modelWithCornersSelf 𝕜 F₁) n (Prod.fst ∘ f) s x ∧
      ContMDiffWithinAt I (modelWithCornersSelf 𝕜 F₂) n (Prod.snd ∘ f) s x
-- Mathlib.Analysis.Convex.DoublyStochasticMatrix
/-- The all-ones row vector multiplied with a doubly stochastic matrix is 1.  -/
one_vecMul_of_mem_doublyStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {M : Matrix n n R},
  M ∈ doublyStochastic R n → Matrix.vecMul 1 M = 1
-- Init.GrindInstances.ToInt
Lean.Grind.instOfNatUSizeUintNumBits : Lean.Grind.ToInt.OfNat USize (Lean.Grind.IntInterval.uint System.Platform.numBits)
-- Init.Data.SInt.Lemmas
Int8.toInt16_ofInt : ∀ {n : ℤ}, Int8.minValue.toInt ≤ n → n ≤ Int8.maxValue.toInt → (Int8.ofInt n).toInt16 = Int16.ofInt n
-- Init.Data.BitVec.Bitblast
/-- Prove that signed division `x.toInt / y.toInt` only overflows when `x = intMin w` and `y = allOnes w` (for `0 < w`).
 -/
BitVec.sdivOverflow_eq : ∀ {w : ℕ} (x y : BitVec w),
  x.sdivOverflow y = (decide (0 < w) && decide (x = BitVec.intMin w) && decide (y = BitVec.allOnes w))
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_fst_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [inst_2 : CategoryTheory.Limits.HasPullback i i]
  [inst_3 : CategoryTheory.Limits.HasPullback f g]
  [inst_4 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)]
  [inst_5 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i)
      (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i)
        (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)]
  {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal i)
          (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i)
            (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp f i)
            (CategoryTheory.CategoryStruct.comp g i))
          h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h
-- Init.Data.Nat.Gcd
Nat.gcd_mul_left_dvd_mul_gcd : ∀ (k m n : ℕ), (m * n).gcd k ∣ m.gcd k * n.gcd k
-- Lean.Elab.Do.Control
Lean.Elab.Do.ControlStack.breakT : Lean.Elab.Do.MonadInfo → Lean.Elab.Do.ControlStack → Lean.Elab.Do.ControlStack
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Γ'.bit0.sizeOf_spec : sizeOf Turing.PartrecToTM2.Γ'.bit0 = 1
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.mul_right : ∀ {α : Type u} {β : Type v} {l : Filter α} [inst : Mul β] {f₁ f₂ f₃ : α → β}, f₁ =ᶠ[l] f₂ → f₁ * f₃ =ᶠ[l] f₂ * f₃
-- Mathlib.Topology.Piecewise
ContinuousOn.piecewise : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {s t : Set α}
  [inst_2 : (a : α) → Decidable (a ∈ t)],
  (∀ a ∈ s ∩ frontier t, f a = g a) →
    ContinuousOn f (s ∩ closure t) → ContinuousOn g (s ∩ closure tᶜ) → ContinuousOn (t.piecewise f g) s
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ \ t₂)[k]? = if k ∈ t₂ then none else t₁[k]?
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.lt_aleph0_iff_set_finite : ∀ {α : Type u} {S : Set α}, Cardinal.mk ↑S < Cardinal.aleph0 ↔ S.Finite
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instDistribSMulForallOfSMul : {M : Type u_1} → {α : Type u_3} → {A : Type u_5} → [SMul M α] → [inst : AddZeroClass A] → DistribSMul Mᵈᵐᵃ (α → A)
-- Init.Data.Int.LemmasAux
Int.blt'_eq_false : ∀ (a b : ℤ), (a.blt' b = false) = ¬a < b
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.id.match_1.splitter : {C : Type u_1} →
  (motive : CategoryTheory.WithTerminal C → Sort u_2) →
    (x : CategoryTheory.WithTerminal C) →
      ((a : C) → motive (CategoryTheory.WithTerminal.of a)) →
        (Unit → motive CategoryTheory.WithTerminal.star) → motive x