mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Order.IntermediateValue
/-- If `f : α → α` is continuous on `[[a, b]]`, `a ≤ f a`, and `f b ≤ b`,
then `f` has a fixed point on `[[a, b]]`.  -/
exists_mem_uIcc_isFixedPt : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a b : α} {f : α → α},
  ContinuousOn f (Set.uIcc a b) → a ≤ f a → f b ≤ b → ∃ c ∈ Set.uIcc a b, Function.IsFixedPt f c
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
SSet.S.le_iff_nonempty_hom : ∀ {X : SSet} (x y : X.S), x ≤ y ↔ Nonempty (SSet.S.equivElements y ⟶ SSet.S.equivElements x)
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Embedding.isContained : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (f : G ↪g H), G.IsContained H
-- Mathlib.Data.Set.Image
/-- **Alias** of `Set.image_sdiff_subset`. -/
Set.image_diff_subset : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s t : Set α), f '' (s \ t) ⊆ f '' s ∩ f '' tᶜ
-- Mathlib.NumberTheory.Ostrowski
Rat.AbsoluteValue.real_eq_abs : ∀ (r : ℚ), Rat.AbsoluteValue.real r = ↑|r|
-- Aesop.Forward.State
Aesop.VariableMap.mk.inj : ∀ {map map_1 : Lean.PHashMap Aesop.PremiseIndex Aesop.InstMap}, { map := map } = { map := map_1 } → map = map_1
-- Init.Data.SInt.Basic
/-- Converts a natural number to an 8-bit signed integer, wrapping around on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:
* `Int8.ofNat 53 = 53`
* `Int8.ofNat 127 = 127`
* `Int8.ofNat 128 = -128`
* `Int8.ofNat 255 = -1`
 -/
Int8.ofNat : ℕ → Int8
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than the given key,
returning `fallback` if no such pair exists.
 -/
Std.DTreeMap.Const.getEntryLTD : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap α (fun x => β) cmp → α → α × β → α × β
-- Lean.Elab.Deriving.Basic
Lean.Elab.DerivingHandler : Type
-- Init.Data.Int.Lemmas
Int.add_right_comm : ∀ (a b c : ℤ), a + b + c = a + c + b
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.im_sub : ∀ {d : ℤ} (z w : ℤ√d), (z - w).im = z.im - w.im
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
/-- The condition that a pseudofunctor satisfies the descent of morphisms
relative to a presieve.  -/
CategoryTheory.Pseudofunctor.IsPrestackFor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat →
      {S : C} → CategoryTheory.Presieve S → Prop
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
/-- A non-empty set with no doubling is the right translate of its stabilizer.  -/
Finset.op_smul_stabilizer_of_no_doubling : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A : Finset G} {a : G},
  (A * A).card ≤ A.card → a ∈ A → MulOpposite.op a • ↑(MulAction.stabilizer G A) = ↑A
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Comonad.Coalgebra.isoMk_hom_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A B : G.Coalgebra}
  (h : A.A ≅ B.A)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp A.a (G.map h.hom) = CategoryTheory.CategoryStruct.comp h.hom B.a)
      CategoryTheory.Comonad.Coalgebra.isoMk._auto_1),
  (CategoryTheory.Comonad.Coalgebra.isoMk h w).hom.f = h.hom
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.coe_nonneg : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [inst : LE β] [inst_1 : Zero β] {f : α → β},
  0 ≤ ↑f ↔ ∀ᶠ (x : α) in l, 0 ≤ f x
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succ?_eq_some : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.InfinitelyUpwardEnumerable α] {a : α},
  Std.PRange.succ? a = some (Std.PRange.succ a)
-- Mathlib.LinearAlgebra.Matrix.ToLin
isStablyFiniteRing_iff_isDedekindFiniteMonoid_moduleEnd : ∀ {A : Type u_3} [inst : Semiring A],
  IsStablyFiniteRing A ↔ ∀ (n : ℕ), IsDedekindFiniteMonoid (Module.End A (Fin n → A))
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List α} {k fallback : α},
      m.contains k = false →
        l.contains k = false →
          (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).getKeyD k fallback = fallback
-- Mathlib.Data.EReal.Basic
instBotEReal : Bot EReal
-- Mathlib.Tactic.Tauto
/-- The core loop of the `tauto` tactic. Repeatedly tries to break down propositions
until no more progress can be made. Tries `assumption` and `contradiction` at every
step, to discharge goals as soon as possible. Does not do anything that requires
backtracking.

TODO: The Lean 3 version uses more-powerful versions of `contradiction` and `assumption`
that additionally apply `symm` and use a fancy union-find data structure to avoid
duplicated work.
 -/
Mathlib.Tactic.Tauto.tautoCore : Lean.Elab.Tactic.TacticM Unit
-- Init.Data.Order.Ord
Option.instOrientedOrd : ∀ {α : Type u_1} [inst : Ord α] [Std.OrientedOrd α], Std.OrientedOrd (Option α)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.rightHomologyMapIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) [inst_2 : S₁.HasRightHomology] [inst_3 : S₂.HasRightHomology],
  (CategoryTheory.ShortComplex.rightHomologyMapIso e).inv = CategoryTheory.ShortComplex.rightHomologyMap e.inv
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.div_div_cancel : ∀ {α : Type u} [inst : DivisionCommMonoid α] {a b : α}, IsUnit a → a / (a / b) = b
-- Std.Data.Iterators.Combinators.Monadic.Zip
_private.Std.Data.Iterators.Combinators.Monadic.Zip.0.Option.SomeLtNone.lt.match_1.splitter : {β : Type u_2} →
  {α : Type u_1} →
    (motive : Option α → Option β → Sort u_3) →
      (x : Option α) →
        (x_1 : Option β) →
          ((x : Option β) → motive none x) →
            ((val : α) → motive (some val) none) → ((x : α) → (y : β) → motive (some x) (some y)) → motive x x_1
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.instAlgebra : {ι : Type u_1} →
  {R' : Type u_2} →
    {R : Type u_3} →
      {A : ι → Type u_4} →
        [inst : CommSemiring R'] →
          [inst_1 : CommSemiring R] →
            [inst_2 : (i : ι) → Semiring (A i)] →
              [Algebra R' R] → [inst_4 : (i : ι) → Algebra R (A i)] → Algebra R' (PiTensorProduct R fun i => A i)
-- Mathlib.Analysis.Asymptotics.TVS
/-- A stronger version of `IsLittleOTVS.congr` that requires the functions only agree along the
filter.  -/
Asymptotics.IsLittleOTVS.congr' : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : Filter α},
  f₁ =o[𝕜; l] g₁ → f₁ =ᶠ[l] f₂ → g₁ =ᶠ[l] g₂ → f₂ =o[𝕜; l] g₂
-- Mathlib.Analysis.Convex.Gauge
/-- **Alias** of `setOfPred_gauge_lt_eq'`. -/
gauge_lt_eq' : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E},
  Absorbent ℝ s → ∀ (a : ℝ), {x | gauge s x < a} = ⋃ r, ⋃ (_ : 0 < r), ⋃ (_ : r < a), r • s
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.exists_mem_range_of_norm_rat_le_one : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (r : ℚ) (h : ‖↑r‖ ≤ 1), ∃ n, 0 ≤ n ∧ n < ↑p ∧ ‖⟨↑r, h⟩ - ↑n‖ < 1
-- Mathlib.Data.Set.Card
Set.encard_eq_one : ∀ {α : Type u_1} {s : Set α}, s.encard = 1 ↔ ∃ x, s = {x}
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.instIsRightCancelMulZeroOfIsCancelAdd : ∀ {R : Type u} [inst : Semiring R] [IsCancelAdd R] [IsRightCancelMulZero R], IsRightCancelMulZero (Polynomial R)
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.eventually_one_sub_smoothingFn_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < 1 - AkraBazziRecurrence.smoothingFn ↑n
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.instIsIso : ∀ {I : Type u₁} {i j : CategoryTheory.Discrete I} (f : i ⟶ j), CategoryTheory.IsIso f
-- Mathlib.GroupTheory.Coprod.Basic
MulEquiv.coprodCongr.eq_1 : ∀ {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N]
  [inst_2 : MulOneClass M'] [inst_3 : MulOneClass N'] (e : M ≃* N) (e' : M' ≃* N'),
  e.coprodCongr e' = (Monoid.Coprod.map ↑e ↑e').toMulEquiv (Monoid.Coprod.map ↑e.symm ↑e'.symm) ⋯ ⋯
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_subsingleton : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Fintype n] [inst_1 : CommSemiring R] [Subsingleton R]
  (A : Matrix m n R), A.rank = 1
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.dominatedFinMeasAdditive_weightedSMul : ∀ {α : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {x : MeasurableSpace α}
  (μ : MeasureTheory.Measure α), MeasureTheory.DominatedFinMeasAdditive μ (MeasureTheory.weightedSMul μ) 1
-- Mathlib.Algebra.Order.Archimedean.Class
/-- Lift a function `M → α` that's monotone along archimedean classes to a
monotone function `ArchimedeanClass M →o α`.  -/
ArchimedeanClass.liftOrderHom : {M : Type u_1} →
  [inst : AddCommGroup M] →
    [inst_1 : LinearOrder M] →
      [inst_2 : IsOrderedAddMonoid M] →
        {α : Type u_2} →
          [inst_3 : PartialOrder α] →
            (f : M → α) →
              (∀ (a b : M), ArchimedeanClass.mk a ≤ ArchimedeanClass.mk b → f a ≤ f b) → ArchimedeanClass M →o α
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.coeFnMonoidHom_apply : ∀ {α : Type u} {R : Type u_2} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] [inst_2 : Monoid R]
  [inst_3 : BoundedMul R] [inst_4 : ContinuousMul R] (a : BoundedContinuousFunction α R) (a_1 : α),
  BoundedContinuousFunction.coeFnMonoidHom a a_1 = a a_1
-- Mathlib.Tactic.Explode.Datatypes
/-- Whether or not to use this in future deps lists. Generally controlled by the `select` function
passed to `explodeCore`. Exception: `∀I` may ignore this for introduced hypotheses.  -/
Mathlib.Explode.Entry.useAsDep : Mathlib.Explode.Entry → Bool
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
/-- This is the non degenerate simplex of a simplicial set which
generates the same subcomplex as a given simplex.  -/
SSet.S.toN : {X : SSet} → X.S → X.N
-- Mathlib.Data.Finsupp.Basic
Finsupp.comapDomain_support : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α → β) (l : β →₀ M)
  (hf : Set.InjOn f (f ⁻¹' ↑l.support)), (Finsupp.comapDomain f l hf).support = l.support.preimage f hf
-- Mathlib.Logic.Equiv.Basic
/-- A subtype of a sigma which pins down the base of the sigma is equivalent to
the respective fiber.  -/
Equiv.sigmaSubtype : {α : Type u_9} → {β : α → Type u_10} → (a : α) → { s // s.fst = a } ≃ β a
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
/-- Club sets are cofinal. If `α` has no maximum, this condition is equivalent to `¬ BddAbove s`.
See `not_bddAbove_iff_isCofinal`.  -/
IsClub.isCofinal : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α}, IsClub s → IsCofinal s
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.mk.inj : ∀ {α : Type u_5} {toField : Field α} {toConditionallyCompleteLinearOrder : ConditionallyCompleteLinearOrder α}
  {toIsOrderedCancelAddMonoid : IsOrderedCancelAddMonoid α} {toZeroLEOneClass : ZeroLEOneClass α}
  {toPosMulStrictMono : PosMulStrictMono α} {toMulPosStrictMono : MulPosStrictMono α} {toField_1 : Field α}
  {toConditionallyCompleteLinearOrder_1 : ConditionallyCompleteLinearOrder α}
  {toIsOrderedCancelAddMonoid_1 : IsOrderedCancelAddMonoid α} {toZeroLEOneClass_1 : ZeroLEOneClass α}
  {toPosMulStrictMono_1 : PosMulStrictMono α} {toMulPosStrictMono_1 : MulPosStrictMono α},
  { toField := toField, toConditionallyCompleteLinearOrder := toConditionallyCompleteLinearOrder,
        toIsOrderedCancelAddMonoid := toIsOrderedCancelAddMonoid, toZeroLEOneClass := toZeroLEOneClass,
        toPosMulStrictMono := toPosMulStrictMono, toMulPosStrictMono := toMulPosStrictMono } =
      { toField := toField_1, toConditionallyCompleteLinearOrder := toConditionallyCompleteLinearOrder_1,
        toIsOrderedCancelAddMonoid := toIsOrderedCancelAddMonoid_1, toZeroLEOneClass := toZeroLEOneClass_1,
        toPosMulStrictMono := toPosMulStrictMono_1, toMulPosStrictMono := toMulPosStrictMono_1 } →
    toField = toField_1 ∧ toConditionallyCompleteLinearOrder = toConditionallyCompleteLinearOrder_1
-- Mathlib.Topology.Order.OrderClosed
Dense.exists_le' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {s : Set α},
  Dense s → (∀ (x : α), IsBot x → x ∈ s) → ∀ (x : α), ∃ y ∈ s, y ≤ x
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.solveCombine : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr →
  Lean.Meta.Grind.Arith.Cutsat.DvdCnstr → Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_lt_one : ∀ {r : ℝ}, r.toNNReal < 1 ↔ r < 1
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
le_neg_add_iff_le : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddLeftMono α] {a b : α}, 0 ≤ -b + a ↔ b ≤ a
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- The isomorphism of corepresentable functors that defines the left unitor for
Day convolution.  -/
CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitorCorepresentingIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            (F : CategoryTheory.Functor C V) →
              ((CategoryTheory.Functor.whiskeringLeft (C × C) C V).obj (CategoryTheory.MonoidalCategory.tensor C)).comp
                  (((CategoryTheory.Functor.whiskeringLeft (CategoryTheory.Discrete PUnit.{1} × C) (C × C) V).obj
                        ((CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).prod
                          (CategoryTheory.Functor.id C))).comp
                    (CategoryTheory.coyoneda.obj
                      (Opposite.op
                        (CategoryTheory.MonoidalCategory.externalProduct
                          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))
                          F)))) ≅
                CategoryTheory.coyoneda.obj (Opposite.op F)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.map_iSup : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {ι : Sort u_5} (f : M →ₙ+ N)
  (s : ι → AddSubsemigroup M), AddSubsemigroup.map f (iSup s) = ⨆ i, AddSubsemigroup.map f (s i)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.isOrdered.eq_1 : ∀ {α : Type u_1} (cmp : α → α → Ordering) (l_2 r_2 : α),
  RBTree.RBNode.isOrdered cmp RBTree.RBNode.nil (some l_2) (some r_2) = decide (cmp l_2 r_2 = Ordering.lt)
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.destruct_join.aux.eq_1 : ∀ {α : Type u}, Stream'.WSeq.destruct_join.aux none = Computation.pure none
-- Init.Data.SInt.Bitwise
instIdempotentOpInt8HOr : Std.IdempotentOp fun x1 x2 => x1 ||| x2
-- Mathlib.Order.RelIso.Basic
RelIso.mk.injEq : ∀ {α : Type u_5} {β : Type u_6} {r : α → α → Prop} {s : β → β → Prop} (toEquiv : α ≃ β)
  (map_rel_iff' : ∀ {a b : α}, s (toEquiv a) (toEquiv b) ↔ r a b) (toEquiv_1 : α ≃ β)
  (map_rel_iff'_1 : ∀ {a b : α}, s (toEquiv_1 a) (toEquiv_1 b) ↔ r a b),
  ({ toEquiv := toEquiv, map_rel_iff' := map_rel_iff' } = { toEquiv := toEquiv_1, map_rel_iff' := map_rel_iff'_1 }) =
    (toEquiv = toEquiv_1)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.Supports.eq_1 : ∀ (S : Finset Turing.PartrecToTM2.Λ') (p : Turing.PartrecToTM2.Γ' → Bool) (k₁ k₂ : Turing.PartrecToTM2.K')
  (q : Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.Λ'.Supports S (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q) = Turing.PartrecToTM2.Λ'.Supports S q
-- Mathlib.Analysis.Normed.Group.Pointwise
vadd_ball_zero : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x : E), x +ᵥ Metric.ball 0 δ = Metric.ball x δ
-- Mathlib.Analysis.Normed.Group.Hom
/-- continuous linear maps are Lipschitz continuous.  -/
NormedAddGroupHom.lipschitz : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f : NormedAddGroupHom V₁ V₂), LipschitzWith ⟨‖f‖, ⋯⟩ ⇑f
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.map_c₄ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) {A : Type v} [inst_1 : CommRing A] (f : R →+* A),
  (W.map f).c₄ = f W.c₄
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cfg.halt.injEq : ∀ (a a_1 : List ℕ), (Turing.ToPartrec.Cfg.halt a = Turing.ToPartrec.Cfg.halt a_1) = (a = a_1)
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearEquiv.range : ∀ {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₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂),
  (↑e).range = ⊤
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.algebraMap_quotient_injective : ∀ {A : Type u_3} [inst : Ring A] {R : Type u_5} [inst_1 : CommRing R] {I : Ideal A} [inst_2 : I.IsTwoSided]
  [inst_3 : Algebra R A], Function.Injective ⇑(algebraMap (R ⧸ Ideal.comap (algebraMap R A) I) (A ⧸ I))
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.injective_coe : ∀ {ι : Type u_1}, Function.Injective BoxIntegral.Box.toSet
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Cache.meta : Lean.Meta.LazyDiscrTree.Cache → Lean.Meta.Cache
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.lsub_empty : ∀ {ι : Type u_3} [h : IsEmpty ι] (f : ι → Ordinal.{max u_4 u_3}), Ordinal.lsub f = 0
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get!_diff_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 = default
-- Mathlib.Algebra.Star.Unitary
mem_unitarySubgroup_iff : ∀ {G : Type u_2} [inst : Group G] [inst_1 : StarMul G] {g : G}, g ∈ unitarySubgroup G ↔ g ∈ unitary G
-- Mathlib.Analysis.Calculus.ContDiff.Basic
contDiff_zero_fun : ∀ {𝕜 : 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] {n : WithTop ℕ∞},
  ContDiff 𝕜 n fun x => 0
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.sieve₀_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {F : CategoryTheory.Functor C D},
  (CategoryTheory.PreZeroHypercover.map F E).sieve₀ = CategoryTheory.Sieve.functorPushforward F E.sieve₀
-- Mathlib.Order.Filter.AtTopBot.Archimedean
Filter.Tendsto.atTop_nsmul_const : ∀ {α : Type u_1} {R : Type u_2} {l : Filter α} {r : R} [inst : AddCommMonoid R] [inst_1 : LinearOrder R]
  [IsOrderedCancelAddMonoid R] [Archimedean R] {f : α → ℕ},
  0 < r → Filter.Tendsto f l Filter.atTop → Filter.Tendsto (fun x => f x • r) l Filter.atTop
-- Init.Data.SInt.Lemmas
ISize.add_left_neg : ∀ (a : ISize), -a + a = 0
-- Mathlib.Topology.Algebra.Order.UpperLower
HasUpperLowerClosure.mk : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α],
  (∀ (s : Set α), IsUpperSet s → IsUpperSet (closure s)) →
    (∀ (s : Set α), IsLowerSet s → IsLowerSet (closure s)) →
      (∀ (s : Set α), IsOpen s → IsOpen ↑(upperClosure s)) →
        (∀ (s : Set α), IsOpen s → IsOpen ↑(lowerClosure s)) → HasUpperLowerClosure α
-- Mathlib.Order.Filter.Pointwise
Filter.instInv.eq_1 : ∀ {α : Type u_2} [inst : Inv α], Filter.instInv = { inv := Filter.map Inv.inv }
-- Mathlib.Topology.MetricSpace.GromovHausdorff
GromovHausdorff.toGHSpace.congr_simp : ∀ (X : Type u) [inst : MetricSpace X] [inst_1 : CompactSpace X] [inst_2 : Nonempty X],
  GromovHausdorff.toGHSpace X = GromovHausdorff.toGHSpace X
-- Mathlib.Order.Bounds.Image
bddBelow_range_pi : ∀ {α : Type u} {ι : Sort x} {π : α → Type u_1} [inst : (a : α) → Preorder (π a)] {F : ι → (a : α) → π a},
  BddBelow (Set.range F) ↔ ∀ (a : α), BddBelow (Set.range fun i => F i a)
-- Mathlib.Topology.Defs.Filter
/-- Specialization forms a preorder on the topological space.  -/
specializationPreorder : (X : Type u_1) → [TopologicalSpace X] → Preorder X
-- Mathlib.Order.Interval.Finset.Basic
/-- A function from a locally finite preorder is antitone if and only if it is antitone when
restricted to pairs satisfying `a ⩿ b`.  -/
antitone_iff_forall_wcovBy : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [LocallyFiniteOrder α] [inst_2 : Preorder β] (f : α → β),
  Antitone f ↔ ∀ (a b : α), a ⩿ b → f b ≤ f a
-- Mathlib.Analysis.CStarAlgebra.Basic
/-- In a C⋆-ring, star preserves the norm.  -/
CStarRing.to_normedStarGroup : ∀ {E : Type u_2} [inst : NonUnitalNormedRing E] [inst_1 : StarRing E] [CStarRing E], NormedStarGroup E
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofCompletionInfo.sizeOf_spec : ∀ (i : Lean.Elab.CompletionInfo), sizeOf (Lean.Elab.Info.ofCompletionInfo i) = 1 + sizeOf i
-- Mathlib.Topology.MetricSpace.Dilation
/-- Ratio of the composition `g.comp f` of two dilations is the product of their ratios. We assume
that the domain `α` of `f` is a nontrivial metric space, otherwise
`Dilation.ratio f = Dilation.ratio (g.comp f) = 1` but `Dilation.ratio g` may have any value.

See also `Dilation.ratio_comp'` for a version that works for more general spaces.  -/
Dilation.ratio_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MetricSpace α] [Nontrivial α] [inst_2 : PseudoEMetricSpace β]
  [inst_3 : PseudoEMetricSpace γ] {g : β →ᵈ γ} {f : α →ᵈ β},
  Dilation.ratio (g.comp f) = Dilation.ratio g * Dilation.ratio f
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.mk₀_sum : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} {ι : Type u_1} [inst_3 : Fintype ι] (f : ι → (X ⟶ Y)),
  CategoryTheory.Abelian.Ext.mk₀ (∑ i, f i) = ∑ i, CategoryTheory.Abelian.Ext.mk₀ (f i)
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- Eta-expanded form of `mvfderiv_sub` -/
mvfderiv_fun_sub : ∀ {𝕜 : 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_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {g g' : M → F} {x : M},
  MDiffAt g x → MDiffAt g' x → (d% fun i => g i - g' i) x = d% g x - d% g' x
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.num_eq_conts_a : ∀ {K : Type u_1} {g : GenContFract K} {n : ℕ} [inst : DivisionRing K], g.nums n = (g.conts n).a
-- Mathlib.Data.List.AList
AList.instDecidableEq : {α : Type u} → {β : α → Type v} → [DecidableEq α] → [(a : α) → DecidableEq (β a)] → DecidableEq (AList β)
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.instNeg : {E : Type u_3} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {Ω : TopologicalSpace.Opens E} →
        {F : Type u_4} →
          [inst_2 : NormedAddCommGroup F] → [inst_3 : NormedSpace ℝ F] → {n : ℕ∞} → Neg (TestFunction Ω F n)
-- Std.Data.ExtHashSet.Lemmas
_private.Std.Data.ExtHashSet.Lemmas.0.Std.ExtHashSet.ext_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m m' : Std.ExtHashSet α}, m = m' ↔ m.inner = m'.inner
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.recover.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer