mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.inv_hom_id_hom : ∀ {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] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] {F G : CategoryTheory.SingleFunctors C D A} (e : F ≅ G) (n : A),
  CategoryTheory.CategoryStruct.comp (e.inv.hom n) (e.hom.hom n) = CategoryTheory.CategoryStruct.id (G.functor n)
-- Mathlib.NumberTheory.NumberField.CMField
/-- The index of the subgroup of `(𝓞 K)ˣ` generated by the real units and the roots of unity is
equal to `1` or `2` (see `NumberField.IsCMField.indexRealUnits_eq_two_iff` for the computation
of this index).
 -/
NumberField.IsCMField.indexRealUnits_eq_one_or_two : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [NumberField.IsCMField K] [NumberField K],
  NumberField.IsCMField.indexRealUnits K = 1 ∨ NumberField.IsCMField.indexRealUnits K = 2
-- Mathlib.Algebra.Order.Ring.Pow
/-- Bernoulli's inequality for `b / a`, written after multiplication by the denominators.

This is a version for a linear ordered semiring.  -/
pow_add_mul_le_add_pow : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : LinearOrder R] [IsOrderedRing R] [ExistsAddOfLE R] {a b : R},
  0 ≤ a → 0 ≤ 2 * a + b → ∀ (n : ℕ), a ^ n + ↑n * a ^ (n - 1) * b ≤ (a + b) ^ n
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.toContinuousMap : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : Zero β] → [inst_2 : TopologicalSpace β] → ZeroAtInftyContinuousMap α β → C(α, β)
-- Aesop.Stats.Basic
Aesop.instInhabitedGoalKind.default : Aesop.GoalKind
-- Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
/-- An alternative phrasing of the explicit equalizer condition, using more categorical language.  -/
CategoryTheory.regularTopology.equalizerCondition_iff_isIso_lift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.Functor Cᵒᵖ (Type u_4)),
  CategoryTheory.regularTopology.EqualizerCondition P ↔
    ∀ (X B : C) (π : X ⟶ B) [CategoryTheory.EffectiveEpi π] [inst_2 : CategoryTheory.Limits.HasPullback π π],
      CategoryTheory.IsIso (CategoryTheory.Limits.equalizer.lift (P.map π.op) ⋯)
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instCancelMonoid : {α : Type u_1} → [CancelMonoid α] → CancelMonoid αᵐᵒᵖ
-- Init.Tactics
/-- `classical tacs` runs `tacs` in a scope where `Classical.propDecidable` is a low priority
local instance.

Note that `classical` is a scoping tactic: it adds the instance only within the
scope of the tactic.
 -/
Lean.Parser.Tactic.classical : Lean.ParserDescr
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_eq_some_getElem!_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited β]
  {a : α}, t.contains a = true → t[a]? = some t[a]!
-- Mathlib.Analysis.LocallyConvex.PointwiseConvergence
PointwiseConvergenceCLM.instLocallyConvexSpace : ∀ {R : Type u_2} {𝕜₁ : Type u_3} {𝕜₂ : Type u_4} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂}
  {E : Type u_7} {F : Type u_8} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F] [inst_8 : Module 𝕜₂ F]
  [inst_9 : Semiring R] [inst_10 : PartialOrder R] [inst_11 : Module R F] [inst_12 : ContinuousConstSMul R F]
  [LocallyConvexSpace R F] [inst_14 : SMulCommClass 𝕜₂ R F], LocallyConvexSpace R (E →SLₚₜ[σ] F)
-- Lean.Util.ParamMinimizer
/-- Adds parameter `i` to current set.
Sets bit `i` to `true` and records that it was added.
 -/
_private.Lean.Util.ParamMinimizer.0.Lean.Util.ParamMinimizer.add : {m : Type → Type} → ℕ → [Monad m] → Lean.Util.ParamMinimizer.M✝ m Unit
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.map₂_whisker_right_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.Pseudofunctor B CategoryTheory.Cat)
  {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c) (X : ↑(self.obj a)),
  (self.map₂ (CategoryTheory.Bicategory.whiskerRight η h)).toNatTrans.app X =
    CategoryTheory.CategoryStruct.comp ((self.mapComp f h).hom.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((self.map h).toFunctor.map ((self.map₂ η).toNatTrans.app X))
        ((self.mapComp g h).inv.toNatTrans.app X))
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mapRange.addEquiv_refl : ∀ {ι : Type u} {β₁ : ι → Type v₁} [inst : (i : ι) → AddZeroClass (β₁ i)],
  (DFinsupp.mapRange.addEquiv fun i => AddEquiv.refl (β₁ i)) = AddEquiv.refl (Π₀ (i : ι), β₁ i)
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.self : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R}, M ≤ IsUnit.submonoid R → IsLocalization M R
-- Init.Data.Array.Lemmas
Array.push_eq_append_iff : ∀ {α : Type u_1} {xs ys zs : Array α} {x : α},
  zs.push x = xs ++ ys ↔ ys = #[] ∧ xs = zs.push x ∨ ∃ ys', ys = ys'.push x ∧ zs = xs ++ ys'
-- Init.Data.Dyadic.Basic
Rat.toRat_toDyadic_le : ∀ {x : ℚ} {prec : ℤ}, (x.toDyadic prec).toRat ≤ x
-- Mathlib.Algebra.Ring.Equiv
/-- By definition, a ring isomorphism preserves the additive structure.  -/
RingEquivClass.map_add : ∀ {F : Type u_7} {R : Type u_8} {S : Type u_9} {inst : Mul R} {inst_1 : Add R} {inst_2 : Mul S} {inst_3 : Add S}
  {inst_4 : EquivLike F R S} [self : RingEquivClass F R S] (f : F) (a b : R), f (a + b) = f a + f b
-- Mathlib.GroupTheory.Perm.Finite
Equiv.Perm.support_pow_coprime : ∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α] {σ : Equiv.Perm α} {n : ℕ},
  n.Coprime (orderOf σ) → (σ ^ n).support = σ.support
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.Products.instLinearOrder : {I : Type u} → [inst : LinearOrder I] → LinearOrder (Profinite.NobelingProof.Products I)
-- Mathlib.Algebra.Order.Archimedean.Class
/-- Adding top to the type of finite classes yields the type of all classes.  -/
FiniteArchimedeanClass.withTopOrderIso : (M : Type u_1) →
  [inst : AddCommGroup M] →
    [inst_1 : LinearOrder M] →
      [inst_2 : IsOrderedAddMonoid M] → WithTop (FiniteArchimedeanClass M) ≃o ArchimedeanClass M
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.isoMk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentData f} (e e_1 : (i : ι) → D₁.obj i ≅ D₂.obj i) (e_e : e = e_1)
  (comm :
    ∀ ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂)
      (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q) (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q),
      CategoryTheory.CategoryStruct.comp ((F.map f₁.op.toLoc).toFunctor.map (e i₁).hom) (D₂.hom q f₁ f₂ ⋯ ⋯) =
        CategoryTheory.CategoryStruct.comp (D₁.hom q f₁ f₂ ⋯ ⋯) ((F.map f₂.op.toLoc).toFunctor.map (e i₂).hom)),
  CategoryTheory.Pseudofunctor.DescentData.isoMk e comm = CategoryTheory.Pseudofunctor.DescentData.isoMk e_1 ⋯
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.instIsStableUnderShiftByTop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (a : A), ⊤.IsStableUnderShiftBy a
-- Init.Data.Array.Zip
_private.Init.Data.Array.Zip.0.List.getElem?_zipWith.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option α → Option β → Sort u_3) (a : α) (b : β)
  (h_1 : (a : α) → (b : β) → motive (some a) (some b)) (h_2 : (x : Option α) → (x_1 : Option β) → motive x x_1),
  (match some a, some b with
    | some a, some b => h_1 a b
    | x, x_1 => h_2 x x_1) =
    h_1 a b
-- Mathlib.Data.Finset.Prod
Finset.card_product : ∀ {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β), (s ×ˢ t).card = s.card * t.card
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.isPath_cons : ∀ {F : PFunctor.{uA, uB}} {xs : PFunctor.Approx.Path F} {a a' : F.A} {f : F.B a → F.M} {i : F.B a'},
  PFunctor.M.IsPath (⟨a', i⟩ :: xs) (PFunctor.M.mk ⟨a, f⟩) → a = a'
-- Init.Data.SInt.Lemmas
Int64.ofBitVec_inj : ∀ {a b : BitVec 64}, Int64.ofBitVec a = Int64.ofBitVec b ↔ a = b
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_dvd_index_of_normal : ∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G) [H.Normal], H.relIndex K ∣ H.index
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- Lists of lists are translated with a `consₗ` after each encoded list.
For example:

```
    [] = []
    [[]] = [consₗ]
    [[], []] = [consₗ, consₗ]
    [[0]] = [cons, consₗ]
    [[1, 2], [0]] = [bit1, cons, bit0, bit1, cons, consₗ, cons, consₗ]
```
 -/
Turing.PartrecToTM2.trLList : List (List ℕ) → List Turing.PartrecToTM2.Γ'
-- Mathlib.Control.Monad.Cont
MonadCont.Label.apply : {α : Type w} → {m : Type u → Type v} → {β : Type u} → MonadCont.Label α m β → α → m β
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.Graph.in₀₂_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {c : γ},
  (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₀ a) (Sum3.in₂ c) ↔ ∃ b, (a, b, c) ∈ t
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reverse_C : ∀ {R : Type u_1} [inst : Semiring R] (t : R), (Polynomial.C t).reverse = Polynomial.C t
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_ofNat_mul_add : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ) [inst_4 : m.AtLeastTwo],
  toIocMod hp a (OfNat.ofNat m * p + b) = toIocMod hp a b
-- Init.Classical
Classical.imp_iff_left_iff : ∀ {b a : Prop}, (b ↔ a → b) ↔ a ∨ b
-- Mathlib.Data.Rat.Lemmas
Rat.natCast_add_den : ∀ (n : ℕ) (q : ℚ), (↑n + q).den = q.den
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Real.continuousAt_rpow_of_pos : ∀ (p : ℝ × ℝ), 0 < p.2 → ContinuousAt (fun p => p.1 ^ p.2) p
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.step_filterMapWithPostcondition.match_3.eq_2 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it' h
-- Mathlib.Algebra.Module.Presentation.Differentials
/-- The presentation of the `S`-module `Ω[S⁄R]` deduced from a presentation
of `S` as an `R`-algebra.  -/
Algebra.Presentation.differentials : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Algebra.Presentation R S ι σ → Module.Presentation S Ω[S⁄R]
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : CommSemiring R] {f : MvPowerSeries σ R},
  MvPowerSeries.constantCoeff f = 0 → Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The upper part of the first column of the snake diagram is exact.  -/
CategoryTheory.ShortComplex.SnakeInput.exact_C₁_up : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C),
  { X₁ := S.L₀.X₁, X₂ := S.L₁.X₁, X₃ := S.L₂.X₁, f := S.v₀₁.τ₁, g := S.v₁₂.τ₁, zero := ⋯ }.Exact
-- Mathlib.CategoryTheory.ObjectProperty.ClosureShift
CategoryTheory.ObjectProperty.instIsStableUnderShiftRetractClosure : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {A : Type u_2}
  [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A] [P.IsStableUnderShift A],
  P.retractClosure.IsStableUnderShift A
-- Lean.Attributes
Lean.instInhabitedEnumAttributes.default : {α : Type} → Lean.EnumAttributes α
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso'_inv_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {T : C}
  (t : CategoryTheory.Limits.IsTerminal T),
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso' X i t).inv.left =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.left).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.left
          (t.from (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
        (CategoryTheory.CategoryStruct.comp ⋯.isoPushout.hom
          (⋯.desc
            (CategoryTheory.Limits.pushout.inl (CategoryTheory.MonoidalCategoryStruct.whiskerRight X.hom I)
              (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.left (t.from I)))
            (CategoryTheory.Limits.pushout.inr (CategoryTheory.MonoidalCategoryStruct.whiskerRight X.hom I)
              (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.left (t.from I)))
            ⋯)))
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Multipliable.tprod_inv₀ : ∀ {α : Type u_1} {K : Type u_4} [inst : CommGroupWithZero K] [inst_1 : TopologicalSpace K] {f : α → K}
  {L : SummationFilter α} [ContinuousInv₀ K] [T2Space K] [L.NeBot],
  Multipliable f L → ∏'[L] (x : α), f x ≠ 0 → ∏'[L] (x : α), (f x)⁻¹ = (∏'[L] (x : α), f x)⁻¹
-- Init.Data.Int.DivMod.Lemmas
Int.fdiv_eq_of_eq_mul_left : ∀ {a b c : ℤ}, b ≠ 0 → a = c * b → a.fdiv b = c
-- Mathlib.Topology.Algebra.InfiniteSum.Real
summable_of_sum_le : ∀ {ι : Type u_3} {f : ι → ℝ} {c : ℝ}, 0 ≤ f → (∀ (u : Finset ι), ∑ x ∈ u, f x ≤ c) → Summable f
-- Lean.Parser.Term.Doc
/-- Recommended spellings for notations, stored in such a way that it is easy to generate a table
containing every recommended spelling exactly once.  -/
Lean.Parser.Term.Doc.recommendedSpellingExt : Lean.PersistentEnvExtension Lean.Parser.Term.Doc.RecommendedSpelling Lean.Parser.Term.Doc.RecommendedSpelling
  (Array Lean.Parser.Term.Doc.RecommendedSpelling)
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- A variant of `Matrix.trace_units_conj'`.  -/
Matrix.trace_conj' : ∀ {m : Type u} {α : Type v} [inst : CommRing α] [inst_1 : Fintype m] [inst_2 : DecidableEq m] {M : Matrix m m α},
  IsUnit M → ∀ (N : Matrix m m α), (M⁻¹ * N * M).trace = N.trace
-- Mathlib.Analysis.Normed.Operator.NormedSpace
LinearIsometry.norm_toContinuousLinearMap : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [NontrivialTopology E] [RingHomIsometric σ₁₂]
  (f : E →ₛₗᵢ[σ₁₂] F), ‖f.toContinuousLinearMap‖ = 1
-- Mathlib.Algebra.Group.AddChar
AddChar.mk.injEq : ∀ {A : Type u_1} [inst : AddMonoid A] {M : Type u_2} [inst_1 : Monoid M] (toFun : A → M)
  (map_zero_eq_one' : toFun 0 = 1) (map_add_eq_mul' : ∀ (a b : A), toFun (a + b) = toFun a * toFun b) (toFun_1 : A → M)
  (map_zero_eq_one'_1 : toFun_1 0 = 1) (map_add_eq_mul'_1 : ∀ (a b : A), toFun_1 (a + b) = toFun_1 a * toFun_1 b),
  ({ toFun := toFun, map_zero_eq_one' := map_zero_eq_one', map_add_eq_mul' := map_add_eq_mul' } =
      { toFun := toFun_1, map_zero_eq_one' := map_zero_eq_one'_1, map_add_eq_mul' := map_add_eq_mul'_1 }) =
    (toFun = toFun_1)
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.entryAtIdx : {α : Type u} → {β : Type v} → (t : Std.DTreeMap.Internal.Impl α fun x => β) → t.Balanced → (n : ℕ) → n < t.size → α × β
-- Mathlib.Topology.Connected.PathConnected
ZerothHomotopy.inhabited : Inhabited (ZerothHomotopy ℝ)
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
GenContFract.of_s_head_aux : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] (v : K),
  (GenContFract.of v).s.get? 0 = (GenContFract.IntFractPair.stream v 1).bind (some ∘ fun p => { a := 1, b := ↑p.b })
-- Mathlib.LinearAlgebra.TensorPower.Symmetric
SymmetricPower.smul : ∀ {R ι : Type u} [inst : CommSemiring R] {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (r : R)
  (x y : PiTensorProduct R fun x => M),
  (addConGen (SymmetricPower.Rel R ι M)) x y → (addConGen (SymmetricPower.Rel R ι M)) (r • x) (r • y)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k a fallback : α} {v : β k},
  (t.insertIfNew k v).getKeyD a fallback = if cmp k a = Ordering.eq ∧ k ∉ t then k else t.getKeyD a fallback
-- Mathlib.MeasureTheory.Measure.Portmanteau
/-- One implication of the portmanteau theorem: if for all open sets `G` we have the liminf
condition `μ(G) ≤ liminf μsₙ(G)`, then the measures `μsₙ` converge weakly to the measure `μ`.
Formulated here for countably generated filters.  -/
MeasureTheory.tendsto_of_forall_isOpen_le_liminf : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {ι : Type u_2} {μ : MeasureTheory.ProbabilityMeasure Ω} {μs : ι → MeasureTheory.ProbabilityMeasure Ω} {L : Filter ι}
  [L.IsCountablyGenerated],
  (∀ (G : Set Ω), IsOpen G → μ G ≤ Filter.liminf (fun i => (μs i) G) L) → Filter.Tendsto (fun i => μs i) L (nhds μ)
-- Mathlib.Tactic.Translate.Core
/-- Run a `ReplacementM` computation, returning the result and the value of `relevant_arg` that
corresponds to this translation.  -/
Mathlib.Tactic.Translate.ReplacementM.run : {α : Type} → Array Lean.FVarId → Array Lean.FVarId → Mathlib.Tactic.Translate.ReplacementM α → Lean.MetaM (α × Option ℕ)
-- Mathlib.Algebra.Order.Quantale
/-- A quantale is a semigroup distributing over a complete lattice.  -/
Quantale : (α : Type u_1) → [inst : Semigroup α] → [inst_1 : CompleteLattice α] → [IsQuantale α] → Type
-- Mathlib.RingTheory.LocalProperties.Exactness
injective_of_isLocalized_maximal : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6)
  [inst_5 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)]
  [inst_6 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module R (Mₚ P)]
  (f : (P : Ideal R) → [inst_7 : P.IsMaximal] → M →ₗ[R] Mₚ P)
  [inst_7 : ∀ (P : Ideal R) [inst_7 : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)]
  (Nₚ : (P : Ideal R) → [P.IsMaximal] → Type u_7) [inst_8 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)]
  [inst_9 : (P : Ideal R) → [inst_9 : P.IsMaximal] → Module R (Nₚ P)]
  (g : (P : Ideal R) → [inst_10 : P.IsMaximal] → N →ₗ[R] Nₚ P)
  [inst_10 : ∀ (P : Ideal R) [inst_10 : P.IsMaximal], IsLocalizedModule.AtPrime P (g P)] (F : M →ₗ[R] N),
  (∀ (P : Ideal R) [inst_11 : P.IsMaximal], Function.Injective ⇑((IsLocalizedModule.map P.primeCompl (f P) (g P)) F)) →
    Function.Injective ⇑F
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.length_toList_roo : ∀ {a b : ℕ}, (a<...b).toList.length = b - a - 1
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instNormedSpace : {A : Type u_1} →
  [inst : NonUnitalCStarAlgebra A] →
    [inst_1 : PartialOrder A] →
      [inst_2 : StarOrderedRing A] →
        {m : Type u_2} →
          {n : Type u_3} → [inst_3 : Fintype m] → [inst_4 : Fintype n] → NormedSpace ℂ (CStarMatrix m n A)
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- The degree of `w ∈ sᶜ` in `G` is at most the degree in `G.between s sᶜ` plus the excluded
vertices from `sᶜ`.  -/
SimpleGraph.degree_le_between_add_compl : ∀ {V : Type u_1} {w : V} {G : SimpleGraph V} [inst : DecidableEq V] [inst_1 : Fintype V] {s : Finset V}
  [inst_2 : DecidableRel G.Adj], w ∈ sᶜ → G.degree w ≤ (SimpleGraph.between (↑s) (↑s)ᶜ G).degree w + sᶜ.card
-- Mathlib.Order.SuccPred.Tree
RootedTree.mem_subtreeOf : ∀ {t : RootedTree} [inst : DecidableEq ↑t] {v : ↑t}, v ∈ t.subtreeOf v
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.map_comp_obj_unop : ∀ {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (U : (TopologicalSpace.Opens ↑Z)ᵒᵖ),
  (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp f g)).obj (Opposite.unop U) =
    (TopologicalSpace.Opens.map f).obj ((TopologicalSpace.Opens.map g).obj (Opposite.unop U))
-- Mathlib.CategoryTheory.Sites.Canonical
/-- The `canonicalTopology` on a category is the finest (largest) topology for which every
representable presheaf is a sheaf.  -/
CategoryTheory.Sheaf.canonicalTopology : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.GrothendieckTopology C
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get_eq : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α],
  m.WF → ∀ {k : α} (h' : m.contains k = true), m.get k h' = k
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Consumer.normal.inj : ∀ {α : Type} {promise promise_1 : IO.Promise (Option α)},
  Std.CloseableChannel.Consumer.normal✝ promise = Std.CloseableChannel.Consumer.normal✝ promise_1 → promise = promise_1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {f : β → β}, (t.modify k f).size = t.size
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getKeyLT!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, t₁.Equiv t₂ → t₁.getKeyLT! k = t₂.getKeyLT! k
-- Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
SSet.modelCategoryQuillen.instIsMultiplicativeFibrations : (HomotopicalAlgebra.fibrations SSet).IsMultiplicative
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
IsCyclic.ext : ∀ {G : Type u_2} [inst : Group G] [Finite G] [IsCyclic G] {d : ℕ} {a b : ZMod d},
  Nat.card G = d → (∀ (t : G), t ^ a.val = t ^ b.val) → a = b
-- Mathlib.CategoryTheory.Category.Cat.Adjunction
/-- The connected components functor  -/
CategoryTheory.Cat.connectedComponents : CategoryTheory.Functor CategoryTheory.Cat (Type u)
-- Mathlib.Data.Int.GCD
_private.Mathlib.Data.Int.GCD.0.Nat.P : ℕ → ℕ → ℕ × ℤ × ℤ → Prop
-- Mathlib.Order.Filter.Pointwise
Filter.add_mul_subset : ∀ {α : Type u_2} [inst : Distrib α] {f g h : Filter α}, (f + g) * h ≤ f * h + g * h
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.mul_self_eq_mul_self_iff : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [StarOrderedRing A]
  [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A]
  [T2Space A] (a b : A),
  autoParam (0 ≤ a) CFC.mul_self_eq_mul_self_iff._auto_1 →
    autoParam (0 ≤ b) CFC.mul_self_eq_mul_self_iff._auto_3 → (a * a = b * b ↔ a = b)