mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubmonoid.addUnits_iInf₂ : ∀ {M : Type u_1} [inst : AddMonoid M] {ι : Sort u_2} {κ : ι → Sort u_3} (f : (i : ι) → κ i → AddSubmonoid M),
  (⨅ i, ⨅ j, f i j).addUnits = ⨅ i, ⨅ j, (f i j).addUnits
-- Mathlib.LinearAlgebra.Matrix.Stochastic
/-- Left multiplication of a column stochastic matrix by a non-negative vector
gives a non-negative vector.  -/
Matrix.nonneg_vecMul_of_mem_colStochastic : ∀ {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} {x : n → R},
  M ∈ Matrix.colStochastic R n → (∀ (i : n), 0 ≤ x i) → ∀ (j : n), 0 ≤ Matrix.vecMul x M j
-- Mathlib.Algebra.Order.Field.Rat
instLinearOrderedCommGroupWithZeroNNRat : LinearOrderedCommGroupWithZero ℚ≥0
-- Mathlib.GroupTheory.Divisible
Prod.divisibleBy.eq_1 : ∀ {β : Type u_3} {B : Type u_4} {B' : Type u_5} [inst : SMul β B] [inst_1 : SMul β B'] [inst_2 : Zero β]
  [inst_3 : AddMonoid B] [inst_4 : AddMonoid B'] [inst_5 : DivisibleBy B β] [inst_6 : DivisibleBy B' β],
  Prod.divisibleBy =
    { div := fun p n => (DivisibleBy.div p.1 n, DivisibleBy.div p.2 n), div_zero := ⋯, div_cancel := ⋯ }
-- Mathlib.Order.Filter.IsBounded
Antitone.frequently_le_map_of_frequently_ge : ∀ {R : Type u_5} {S : Type u_6} {F : Filter R} [inst : LinearOrder R] [inst_1 : LinearOrder S] {f : R → S},
  Antitone f → ∀ {l : R}, (∃ᶠ (x : R) in F, l ≤ x) → ∃ᶠ (y : S) in Filter.map f F, y ≤ f l
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_toArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}, t.WF → t.toArray.size = t.size
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.BuilderOption.pattern.sizeOf_spec : ∀ (stx : Lean.Term), sizeOf (Aesop.Frontend.BuilderOption.pattern stx) = 1 + sizeOf stx
-- Mathlib.Analysis.Real.Sqrt
NNReal.sqrt_mul : ∀ (x y : NNReal), NNReal.sqrt (x * y) = NNReal.sqrt x * NNReal.sqrt y
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_filter_not_contains_of_contains_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k : α}
  {fallback : β k},
  Std.Internal.List.DistinctKeys l₁ →
    l₂.contains k = true →
      Std.Internal.List.getValueCastD k (List.filter (fun p => !l₂.contains p.fst) l₁) fallback = fallback
-- Mathlib.Data.Nat.Nth
/-- `Nat.nth p` is the greatest monotone function whose image contains `Set.ofPred p`.  -/
Nat.le_nth_of_monotoneOn_of_surjOn : ∀ {p : ℕ → Prop} (f : ℕ → ℕ),
  Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < hf.toFinset.card} (Set.ofPred p) →
    MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < hf.toFinset.card} →
      ∀ {n : ℕ}, (∀ (hf : (Set.ofPred p).Finite), n < hf.toFinset.card) → f n ≤ Nat.nth p n
-- Mathlib.GroupTheory.Congruence.Hom
/-- The uniqueness part of the universal property for quotients of `AddMonoid`s.  -/
AddCon.lift_unique : ∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] {c : AddCon M} {f : M →+ P}
  (H : c ≤ AddCon.ker f) (g : c.Quotient →+ P), g.comp c.mk' = f → g = c.lift f H
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.copy.injEq : ∀ (q q_1 : Turing.PartrecToTM2.Λ'), (q.copy = q_1.copy) = (q = q_1)
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderTriple.ne_zero : ∀ {p q r : NNReal}, p.HolderTriple q r → p ≠ 0
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.isWeierstrassDivision_weierstrassDiv_weierstrassMod : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] (f : PowerSeries A) {g : PowerSeries A},
  (PowerSeries.map (IsLocalRing.residue A)) g ≠ 0 →
    ∀ [inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A], f.IsWeierstrassDivision g (f /ʷ g) (f %ʷ g)
-- Mathlib.Topology.Algebra.Algebra
/-- Restrict the codomain of a continuous algebra homomorphism `f` to `f.range`.  -/
ContinuousAlgHom.rangeRestrict : {R : Type u_1} →
  [inst : CommSemiring R] →
    {A : Type u_2} →
      [inst_1 : Semiring A] →
        [inst_2 : TopologicalSpace A] →
          {B : Type u_3} →
            [inst_3 : Semiring B] →
              [inst_4 : TopologicalSpace B] →
                [inst_5 : Algebra R A] → [inst_6 : Algebra R B] → (f : A →A[R] B) → A →A[R] ↥(↑f).range
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.forget₂Mon_obj_X : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : CategoryTheory.AddGrp C), ((CategoryTheory.AddGrp.forget₂Mon C).obj A).X = A.X
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.exp_angleDiff_mul : ∀ {x y : Circle}, Circle.exp (x.angleDiff y) * x = y
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- A finite product of functions monotone on `u` is monotone on `u`.  -/
MonotoneOn.finsetProd' : ∀ {ι : Type u_1} {N : Type u_5} [inst : CommMonoid N] [inst_1 : Preorder N] {s : Finset ι} [MulLeftMono N]
  {γ : Type u_9} [inst_3 : Preorder γ] {u : Set γ} {f : ι → γ → N},
  (∀ i ∈ s, MonotoneOn (f i) u) → MonotoneOn (fun x => ∏ i ∈ s, f i x) u
-- Mathlib.Analysis.MeanInequalities
NNReal.geom_mean_le_arith_mean4_weighted : ∀ (w₁ w₂ w₃ w₄ p₁ p₂ p₃ p₄ : NNReal),
  w₁ + w₂ + w₃ + w₄ = 1 → p₁ ^ ↑w₁ * p₂ ^ ↑w₂ * p₃ ^ ↑w₃ * p₄ ^ ↑w₄ ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃ + w₄ * p₄
-- Mathlib.Order.CompleteLattice.Defs
sSup_lt_iff : ∀ {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {l : α}, sSup s < l ↔ ∃ b < l, b ∈ upperBounds s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_alter!_eq_add_one : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      k ∉ t →
        (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true →
          (Std.DTreeMap.Internal.Impl.Const.alter! k f t).size = t.size + 1
-- Init.Data.String.Basic
/-- Advances a valid position on a string to the next valid position, or panics if the given
position is the past-the-end position.  -/
String.Pos.next! : {s : String} → s.Pos → s.Pos
-- Mathlib.Analysis.Meromorphic.LogDeriv
/-- Away from a codiscrete subset of `U`, the logarithmic derivative of the `n`-th power of a
meromorphic function is `n` times the logarithmic derivative.
 -/
MeromorphicOn.logDeriv_zpow_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f : 𝕜 → 𝕜'} {U : Set 𝕜},
  MeromorphicOn f U → ∀ (n : ℤ), logDeriv (f ^ n) =ᶠ[Filter.codiscreteWithin U] n • logDeriv f
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Measurable.sumMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m : MeasurableSpace α} {mβ : MeasurableSpace β}
  {x : MeasurableSpace γ} {x_1 : MeasurableSpace δ} {f : α → β} {g : γ → δ},
  Measurable f → Measurable g → Measurable (Sum.map f g)
-- Mathlib.RingTheory.Ideal.Maps
Ideal.isMaximal_comap_iff_of_bijective : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [inst_3 : RingHomClass F R S], Function.Bijective ⇑f → ∀ {K : Ideal S}, (Ideal.comap f K).IsMaximal ↔ K.IsMaximal
-- Init.Data.String.Basic
String.Slice.Pos.mk.congr_simp : ∀ {s : String.Slice} (offset offset_1 : String.Pos.Raw) (e_offset : offset = offset_1)
  (isValidForSlice : String.Pos.Raw.IsValidForSlice s offset),
  { offset := offset, isValidForSlice := isValidForSlice } = { offset := offset_1, isValidForSlice := ⋯ }
-- Init.Data.Range.Polymorphic.SInt
Int32.instRxiLawfulHasSize : Std.Rxi.LawfulHasSize Int32
-- Mathlib.Order.Ideal
Order.Ideal.coe_toLowerSet : ∀ {P : Type u_1} [inst : LE P] (s : Order.Ideal P), ↑s.toLowerSet = ↑s
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
/-- A terminal object is terminal.  -/
CategoryTheory.Limits.terminalIsTerminal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasTerminal C] → CategoryTheory.Limits.IsTerminal (⊤_ C)
-- Mathlib.Algebra.FiniteSupport.Basic
/-- Eta-expanded form of `Function.HasFiniteSupport.mul_left` -/
Function.HasFiniteSupport.fun_mul_left : ∀ {α : Type u_1} {M : Type u_4} [inst : MulZeroClass M] {f : α → M},
  Function.HasFiniteSupport f → ∀ (g : α → M), Function.HasFiniteSupport fun i => f i * g i
-- Mathlib.Order.Basic
Subtype.mk_lt_mk : ∀ {α : Type u_2} [inst : LT α] {p : α → Prop} {x y : α} {hx : p x} {hy : p y}, ⟨x, hx⟩ < ⟨y, hy⟩ ↔ x < y
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.nullMeasurableSet_toMeasurable : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.NullMeasurableSet (MeasureTheory.toMeasurable μ s) μ
-- Mathlib.Analysis.Normed.Group.Basic
ball_eq_norm_neg_add_lt : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (y : E) (ε : ℝ), Metric.ball y ε = {x | ‖-x + y‖ < ε}
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.ext_iff : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  {f g : AbsoluteValue R S}, f = g ↔ ∀ (x : R), f x = g x
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.neighborSet_completeEquipartiteGraph : ∀ {r t : ℕ} (v : Fin r × Fin t), (SimpleGraph.completeEquipartiteGraph r t).neighborSet v = {v.1}ᶜ ×ˢ Set.univ
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_addNat_Ici : ∀ {n : ℕ} (m : ℕ) (i : Fin n), Finset.image (fun x => x.addNat m) (Finset.Ici i) = Finset.Ici (i.addNat m)
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.piCongrLeft_apply_apply : ∀ {ι : Type u_4} {ι' : Type u_5} {X : ι' → Type u_6} [inst : (j : ι') → UniformSpace (X j)] (e : ι ≃ ι')
  (x : (i : ι) → X (e i)) (i : ι), (UniformEquiv.piCongrLeft e) x (e i) = x i
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.coeff_scaleRoots_natDegree : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) (s : R), (p.scaleRoots s).coeff p.natDegree = p.leadingCoeff
-- Mathlib.LinearAlgebra.FreeModule.PID
/-- If `M` is finite free over a PID `R`, then any submodule `N` is free
and we can find a basis for `M` and `N` such that the inclusion map is a diagonal matrix
in Smith normal form.

This is a strengthening of `Submodule.basisOfPid`.

See also `Ideal.smithNormalForm`, which moreover proves that the dimension of
an ideal is the same as the dimension of the whole ring.
 -/
Submodule.smithNormalForm : {ι : Type u_1} →
  {R : Type u_2} →
    [inst : CommRing R] →
      {M : Type u_3} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [IsDomain R] →
              [IsPrincipalIdealRing R] →
                [Finite ι] → Module.Basis ι R M → (N : Submodule R M) → (n : ℕ) × Module.Basis.SmithNormalForm N ι n
-- Init.Data.Slice.InternalLemmas
Std.Slice.Internal.toListRev_eq_toListRev_iter : ∀ {γ : Type u} {α β : Type v} {s : Std.Slice γ} [inst : Std.ToIterator (Std.Slice γ) Id α β]
  [inst_1 : Std.Iterator α Id β] [Std.Iterators.Finite α Id], s.toListRev = (Std.Slice.Internal.iter s).toListRev
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
ContinuousAt.clog : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℂ} {x : α},
  ContinuousAt f x → f x ∈ Complex.slitPlane → ContinuousAt (fun t => Complex.log (f t)) x
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.s.eq_1 : LucasLehmer.s 0 = 4
-- Mathlib.Control.Fold
Monoid.Foldr.ofFreeMonoid_apply : ∀ {α β : Type u} (f : α → β → β) (xs : FreeMonoid α),
  (Monoid.Foldr.ofFreeMonoid f) xs = TypeCat.ofHom (flip (List.foldr f) (FreeMonoid.toList xs))
-- Mathlib.Control.EquivFunctor
/-- An `EquivFunctor` in fact takes every equiv to an equiv.  -/
EquivFunctor.mapEquiv : (f : Type u₀ → Type u₁) → [EquivFunctor f] → {α β : Type u₀} → α ≃ β → f α ≃ f β
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
/-- If `f : P ⟶ R` and `g : Q ⟶ R` are morphisms and `p : P` and `q : Q` are pseudoelements such
that `f p = g q`, then there is some `s : pullback f g` such that `fst s = p` and `snd s = q`.

Remark: Borceux claims that `s` is unique, but this is false. See
`Counterexamples/Pseudoelement.lean` for details.  -/
CategoryTheory.Abelian.Pseudoelement.pseudo_pullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {P Q R : C} {f : P ⟶ R} {g : Q ⟶ R}
  {p : CategoryTheory.Abelian.Pseudoelement P} {q : CategoryTheory.Abelian.Pseudoelement Q},
  CategoryTheory.Abelian.Pseudoelement.pseudoApply f p = CategoryTheory.Abelian.Pseudoelement.pseudoApply g q →
    ∃ s,
      CategoryTheory.Abelian.Pseudoelement.pseudoApply (CategoryTheory.Limits.pullback.fst f g) s = p ∧
        CategoryTheory.Abelian.Pseudoelement.pseudoApply (CategoryTheory.Limits.pullback.snd f g) s = q
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.rightUnshift_units_smul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {R : Type u_1}
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C] {K L : CochainComplex C ℤ} {n' a : ℤ}
  (γ : CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') (n : ℤ)
  (hn : n' + a = n) (x : Rˣ), (x • γ).rightUnshift n hn = x • γ.rightUnshift n hn
-- Mathlib.Algebra.Algebra.Unitization
Unitization.isStarNormal_inr : ∀ {R : Type u_1} {A : Type u_2} [inst : Semiring R] [inst_1 : StarAddMonoid R] [inst_2 : Star A] {a : A}
  [inst_3 : AddCommMonoid A] [inst_4 : Mul A] [inst_5 : SMulWithZero R A], IsStarNormal ↑a ↔ IsStarNormal a
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.endsWith_prop_eq_false_iff_get : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String},
  s.endsWith P = false ↔ ∀ (h : s.endPos ≠ s.startPos), ¬P ((s.endPos.prev h).get ⋯)
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
ModelWithCorners.uniqueMDiffOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H),
  UniqueMDiff[Set.range ↑I]
-- Mathlib.Algebra.Star.NonUnitalSubsemiring
/-- The `carrier` of a `StarSubset` is closed under the `star` operation.  -/
SubStarSemigroup.star_mem' : ∀ {M : Type v} [inst : Mul M] [inst_1 : Star M] (self : SubStarSemigroup M) {a : M},
  a ∈ self.carrier → star a ∈ self.carrier
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instNonUnitalCommRingQuotient : {R : Type u_1} → [inst : NonUnitalCommRing R] → (c : RingCon R) → NonUnitalCommRing c.Quotient
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
CategoryTheory.Limits.PreservesPullback.iso_hom_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_2 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G]
  [inst_3 : CategoryTheory.Limits.HasPullback f g] [inst_4 : CategoryTheory.Limits.HasPullback (G.map f) (G.map g)]
  {Z_1 : D} (h : G.obj X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPullback.iso G f g).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (G.map f) (G.map g)) h) =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pullback.fst f g)) h
-- Lean.Environment
Lean.Kernel.Exception.declHasMVars.injEq : ∀ (env : Lean.Kernel.Environment) (name : Lean.Name) (expr : Lean.Expr) (env_1 : Lean.Kernel.Environment)
  (name_1 : Lean.Name) (expr_1 : Lean.Expr),
  (Lean.Kernel.Exception.declHasMVars env name expr = Lean.Kernel.Exception.declHasMVars env_1 name_1 expr_1) =
    (env = env_1 ∧ name = name_1 ∧ expr = expr_1)
-- Mathlib.NumberTheory.ArithmeticFunction.LFunction
/-- In `ArithmeticFunction.ofPowerSeries`, replacing the base `q` with a power `q ^ k` corresponds
to substituting `X` with `X ^ k` in the original power series.  -/
ArithmeticFunction.ofPowerSeries_pow : ∀ {R : Type u_1} [inst : CommRing R] (q : ℕ) {k : ℕ},
  k ≠ 0 →
    ∀ (f : PowerSeries R),
      (ArithmeticFunction.ofPowerSeries (q ^ k)) f =
        (ArithmeticFunction.ofPowerSeries q) (PowerSeries.subst (PowerSeries.X ^ k) f)
-- Mathlib.Data.EReal.Operations
EReal.bot_mul_coe_of_pos : ∀ {x : ℝ}, 0 < x → ⊥ * ↑x = ⊥
-- Mathlib.CategoryTheory.Functor.OfSequence
/-- The functor `ℕ ⥤ C` constructed from a sequence of
morphisms `f : X n ⟶ X (n + 1)` for all `n : ℕ`.  -/
CategoryTheory.Functor.ofSequence : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → {X : ℕ → C} → ((n : ℕ) → X n ⟶ X (n + 1)) → CategoryTheory.Functor ℕ C
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.map_eq : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (φ : W.LeftFraction X Y) (L : CategoryTheory.Functor C D) [inst_2 : L.IsLocalization W],
  φ.map L ⋯ = CategoryTheory.CategoryStruct.comp (L.map φ.f) (CategoryTheory.Localization.isoOfHom L W φ.s ⋯).inv
-- Mathlib.Data.Set.Subsingleton
Set.not_nontrivial_singleton : ∀ {α : Type u} {x : α}, ¬{x}.Nontrivial
-- Mathlib.Util.Superscript
Mathlib.Tactic.subscriptTerm.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.add_one_sub_one_of_two_dvd : ∀ {R : Type u_1} [inst : CommRing R] {x : R}, 2 ∣ x → IsRelPrime (x + 1) (x - 1)
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_2 : HSub Std.Time.Nanosecond.Offset Std.Time.Minute.Offset Std.Time.Nanosecond.Offset
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.le_comap_map : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : AffineSubspace k P₁),
  s ≤ AffineSubspace.comap f (AffineSubspace.map f s)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_filter!_of_getKey?_eq_some : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β] {f : α → β → Bool} {k k' : α},
  t.WF →
    t.getKey? k = some k' →
      Std.DTreeMap.Internal.Impl.Const.get! (Std.DTreeMap.Internal.Impl.filter! f t) k =
        (Option.filter (fun x => f k' x) (Std.DTreeMap.Internal.Impl.Const.get? t k)).get!
-- Mathlib.Data.Nat.Choose.Multinomial
List.toFinsupp_sum : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : DecidableEq α] (l : List α), (l.toFinsupp.sum fun x a => a) = l.sum
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X₀ : C} {succ : C → C} {toSucc : (X : C) → X ⟶ succ X}
  {X₀_1 : C} {succ_1 : C → C} {toSucc_1 : (X : C) → X ⟶ succ_1 X},
  { X₀ := X₀, succ := succ, toSucc := toSucc } = { X₀ := X₀_1, succ := succ_1, toSucc := toSucc_1 } →
    X₀ = X₀_1 ∧ succ = succ_1 ∧ toSucc ≍ toSucc_1
-- Mathlib.Data.Set.Subsingleton
/-- **Alias** of the reverse direction of `Set.nontrivial_coe_sort`.

---

`s`, coerced to a type, is a nontrivial type if and only if `s` is a nontrivial set.  -/
Set.Nontrivial.coe_sort : ∀ {α : Type u} {s : Set α}, s.Nontrivial → Nontrivial ↑s
-- Mathlib.Computability.RecursiveIn
Nat.RecursiveIn.below.rfind : ∀ {O : Set (ℕ →. ℕ)} {motive : (a : ℕ →. ℕ) → Nat.RecursiveIn O a → Prop} {f : ℕ →. ℕ} (hf : Nat.RecursiveIn O f),
  Nat.RecursiveIn.below hf → motive f hf → Nat.RecursiveIn.below ⋯
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.fst : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace β] [inst_1 : TopologicalSpace γ]
  {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β × γ},
  MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable (fun x => (f x).1) μ
-- Mathlib.Order.Filter.Pointwise
Filter.zero_smul_filter : ∀ {α : Type u_2} {β : Type u_3} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β] {g : Filter β},
  g.NeBot → 0 • g = 0
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- If two ring homomorphisms from `R[M]` are equal on all `single m 1`
and `single 1 r`, then they are equal.

See note [partially-applied ext lemmas].  -/
MonoidAlgebra.ringHom_ext' : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : MulOneClass M] [inst_2 : Semiring S]
  {f g : MonoidAlgebra R M →+* S},
  f.comp MonoidAlgebra.singleOneRingHom = g.comp MonoidAlgebra.singleOneRingHom →
    (↑f).comp (MonoidAlgebra.of R M) = (↑g).comp (MonoidAlgebra.of R M) → f = g
-- Mathlib.Data.Int.Init
/-- The modulus of an integer by another as a natural. Uses the E-rounding convention.  -/
Int.natMod : ℤ → ℤ → ℕ
-- Mathlib.Order.LiminfLimsup
OrderIso.apply_bliminf : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CompleteLattice α] {f : Filter β} {p : β → Prop} {u : β → α}
  [inst_1 : CompleteLattice γ] (e : α ≃o γ), e (Filter.bliminf u f p) = Filter.bliminf (⇑e ∘ u) f p
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
/-- This lemma is useful in non-cancellative monoids, like sets under pointwise operations.  -/
nsmul_le_nsmul_add_of_sq_le_add : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddRightMono M] [AddLeftMono M] {a b : M},
  2 • a ≤ b + a → ∀ {n : ℕ}, n ≠ 0 → n • a ≤ (n - 1) • b + a
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.instAddCommGroup : {ι : Type v} → {β : ι → Type w} → [inst : (i : ι) → AddCommGroup (β i)] → AddCommGroup (DirectSum ι β)
-- Mathlib.InformationTheory.KullbackLeibler.KLFun
InformationTheory.tendsto_rightDeriv_klFun_atTop : Filter.Tendsto (fun x => derivWithin InformationTheory.klFun (Set.Ioi x) x) Filter.atTop Filter.atTop
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.instTrans : {R : Type u_1} →
  [inst : Ring R] →
    {M : Type u_4} →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {U : Submodule R M} → Trans (SModEq U) (SModEq U) (SModEq U)
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.ae_smul_measure_eq : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {R : Type u_8} [inst : Semiring R] [IsDomain R] [inst_2 : Module R ENNReal]
  [inst_3 : IsScalarTower R ENNReal ENNReal] [Module.IsTorsionFree R ENNReal] {c : R},
  c ≠ 0 → ∀ (μ : MeasureTheory.Measure α), MeasureTheory.ae (c • μ) = MeasureTheory.ae μ
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.preimage_add_right_zero' : ∀ {α : Type u_2} [inst : AddGroup α] {b : α}, (fun x => x + -b) ⁻¹' 0 = {b}
-- Mathlib.Data.Stream.Init
Stream'.tails_eq : ∀ {α : Type u} (s : Stream' α), s.tails = Stream'.cons s.tail s.tail.tails
-- Mathlib.LinearAlgebra.Dimension.RankNullity
HasRankNullity.exists_set_linearIndependent : ∀ {R : Type v} {inst : Ring R} [self : HasRankNullity.{u, v} R] (M : Type u) [inst_1 : AddCommGroup M]
  [inst_2 : Module R M], ∃ s, Cardinal.mk ↑s = Module.rank R M ∧ LinearIndepOn R id s
-- Mathlib.RepresentationTheory.Basic
/-- **Alias** of `Representation.asAlgebraHom_ofMulAction_smul_eq_mul`. -/
Representation.ofMulAction_self_smul_eq_mul : ∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [inst_1 : Group G] (x y : MonoidAlgebra k G),
  ((Representation.ofMulAction k G G).asAlgebraHom x) y = x * y
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray_fold_fn.eq_2 : ∀ {n : ℕ} (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment)
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n),
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray_fold_fn assignments (some c) =
    match c.isUnit with
    | none => assignments
    | some (l, true) => assignments.modify (↑l) Std.Tactic.BVDecide.LRAT.Internal.Assignment.addPosAssignment
    | some (l, false) => assignments.modify (↑l) Std.Tactic.BVDecide.LRAT.Internal.Assignment.addNegAssignment
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get_congr : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h : m.WF) {k₁ k₂ : α} (h' : (k₁ == k₂) = true) (h₁ : k₁ ∈ m), m.get k₁ h₁ = m.get k₂ ⋯