mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
/-- The base change isomorphism underlying `IsBaseChange.linearMapRight`  -/
IsBaseChange.linearMapRightBaseChangeEquiv : {R : Type u_1} →
  [inst : CommSemiring R] →
    {S : Type u_2} →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          (M : Type u_3) →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : Module R M] →
                {N : Type u_4} →
                  [inst_5 : AddCommMonoid N] →
                    [inst_6 : Module R N] →
                      {P : Type u_5} →
                        [inst_7 : AddCommMonoid P] →
                          [inst_8 : Module R P] →
                            [inst_9 : Module S P] →
                              [inst_10 : IsScalarTower R S P] →
                                [Module.Free R M] →
                                  [Module.Finite R M] →
                                    {ε : N →ₗ[R] P} → IsBaseChange S ε → TensorProduct R S (M →ₗ[R] N) ≃ₗ[S] M →ₗ[R] P
-- Mathlib.Topology.Instances.AddCircle.Real
/-- The action on `ℝ` by right multiplication of its the subgroup `zmultiples p` (the multiples of
`p:ℝ`) is properly discontinuous.  -/
AddCircle.instProperlyDiscontinuousVAddSubtypeAddOppositeRealMemAddSubgroupOpZmultiples : ∀ (p : ℝ), ProperlyDiscontinuousVAdd ↥(AddSubgroup.zmultiples p).op ℝ
-- Mathlib.Algebra.Module.LinearMap.End
RingEquiv.moduleEndSelf_symm_apply : ∀ (R : Type u_1) [inst : Semiring R] (f : Module.End R R), (RingEquiv.moduleEndSelf R).symm f = MulOpposite.op (f 1)
-- Mathlib.Data.Nat.Factorization.Basic
Nat.Prime.dvd_iff_one_le_factorization : ∀ {p n : ℕ}, Nat.Prime p → n ≠ 0 → (p ∣ n ↔ 1 ≤ n.factorization p)
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
CategoryTheory.PreZeroHypercover.saturate_Y : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  (x x_1 : E.I₀) (r : E.Relation x x_1), E.saturate.Y r = r.obj
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
IsConjRoot.comm : ∀ {R : Type u_1} {A : Type u_5} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {x y : A},
  IsConjRoot R x y ↔ IsConjRoot R y x
-- Mathlib.Tactic.Positivity.Core
_private.Mathlib.Tactic.Positivity.Core.0.Mathlib.Meta.Positivity.OrderRel.ne.sizeOf_spec : sizeOf Mathlib.Meta.Positivity.OrderRel.ne✝ = 1
-- Mathlib.Algebra.GCDMonoid.Basic
Associates.dvd_out_iff : ∀ {α : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] (a : α) (b : Associates α),
  a ∣ b.out ↔ Associates.mk a ≤ b
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.distortion_top : ∀ {ι : Type u_1} [inst : Fintype ι] (I : BoxIntegral.Box ι), ⊤.distortion = I.distortion
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
mulRothNumber_spec : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] (s : Finset α),
  ∃ t ⊆ s, t.card = mulRothNumber s ∧ ThreeGPFree ↑t
-- Mathlib.Analysis.Real.Cardinality
/-- The cardinality of the interval $(-∞, a)$.  -/
Cardinal.mk_Iio_real : ∀ (a : ℝ), Cardinal.mk ↑(Set.Iio a) = Cardinal.continuum
-- Mathlib.Order.Hom.Lattice
InfHom.instBot.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : SemilatticeInf β] [inst_2 : Bot β],
  InfHom.instBot = { bot := InfHom.const α ⊥ }
-- Std.Http.Data.URI.Encoding
_private.Std.Http.Data.URI.Encoding.0.Std.Http.URI.EncodedString.mk.inj : ∀ {r : UInt8 → Bool} {toByteArray : ByteArray} {valid : Std.Http.URI.IsAllowedEncodedChars r toByteArray}
  {toByteArray_1 : ByteArray} {valid_1 : Std.Http.URI.IsAllowedEncodedChars r toByteArray_1},
  { toByteArray := toByteArray, valid := valid } = { toByteArray := toByteArray_1, valid := valid_1 } →
    toByteArray = toByteArray_1
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
/-- If there exists a morphism `a → b` in a free groupoid, then there also exists a zigzag
from `a` to `b` in the generating quiver.  -/
IsFreeGroupoid.path_nonempty_of_hom : ∀ {G : Type u} [inst : CategoryTheory.Groupoid G] [inst_1 : IsFreeGroupoid G] {a b : G},
  Nonempty (a ⟶ b) → Nonempty (Quiver.Path (IsFreeGroupoid.symgen✝ a) (IsFreeGroupoid.symgen✝ b))
-- Mathlib.Data.Countable.Basic
instCountablePSum : ∀ {α : Sort u} {β : Sort v} [Countable α] [Countable β], Countable (α ⊕' β)
-- Mathlib.Order.Hom.Lattice
/-- The underlying function of an `InfHom`.

Do not use this function directly. Instead use the coercion coming from the `FunLike`
instance.  -/
InfHom.toFun : {α : Type u_6} → {β : Type u_7} → [inst : Min α] → [inst_1 : Min β] → InfHom α β → α → β
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.performRatCheck.match_3.eq_1 : ∀ {n : ℕ} (motive : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n → ℕ × Array ℕ → Sort u_1)
  (clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)))
  (rupUnits ratUnits : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)))
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (id : ℕ) (rupHints : Array ℕ)
  (h_1 :
    (clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n))) →
      (rupUnits ratUnits : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) →
        (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) →
          (id : ℕ) →
            (rupHints : Array ℕ) →
              motive { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments }
                (id, rupHints)),
  (match { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments },
      (id, rupHints) with
    | { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments }, (id, rupHints) =>
      h_1 clauses rupUnits ratUnits assignments id rupHints) =
    h_1 clauses rupUnits ratUnits assignments id rupHints
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
isAddCyclic_iff_exists_addOrderOf_eq_natCard : ∀ {α : Type u_1} [inst : AddGroup α] [Finite α], IsAddCyclic α ↔ ∃ g, addOrderOf g = Nat.card α
-- Mathlib.Topology.Order.WithTop
/-- Homeomorphism between the non-bot elements of `WithBot ι` and `ι`.  -/
WithBot.neBotHomeomorph : (ι : Type u_1) → [inst : LinearOrder ι] → [inst_1 : TopologicalSpace ι] → [inst_2 : OrderTopology ι] → ↑{a | a ≠ ⊥} ≃ₜ ι
-- Mathlib.CategoryTheory.Limits.IsConnected
/-- The cocone on `constPUnitFunctor` with cone point `PUnit`.  -/
CategoryTheory.Limits.Types.pUnitCocone : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Limits.Cocone (CategoryTheory.Limits.Types.constPUnitFunctor C)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.ofArrows.mk' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {ι : Type u_1} {Y : ι → C} {f : (i : ι) → Y i ⟶ X}
  {Z : C} {g : Z ⟶ X} (i : ι) (h : Z = Y i),
  g = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) (f i) → CategoryTheory.Presieve.ofArrows Y f g
-- Mathlib.Topology.UniformSpace.UniformEmbedding
uniformly_extend_spec : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace α] [inst_1 : UniformSpace β]
  [inst_2 : UniformSpace γ] {e : β → α} (h_e : IsUniformInducing e) (h_dense : DenseRange e) {f : β → γ},
  UniformContinuous f → ∀ [CompleteSpace γ] (a : α), Filter.Tendsto f (Filter.comap e (nhds a)) (nhds (⋯.extend f a))
-- Mathlib.Logic.Lemmas
ite_dite_distrib_right : ∀ {α : Sort u_1} {p q : Prop} [inst : Decidable p] [inst_1 : Decidable q] {a : q → α} {b : ¬q → α} {c : α},
  (if p then dite q a b else c) = if hq : q then if p then a hq else c else if p then b hq else c
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.mem_atTop_sets : ∀ {α : Type u_3} [inst : Preorder α] [IsDirectedOrder α] [Nonempty α] {s : Set α},
  s ∈ Filter.atTop ↔ ∃ a, ∀ (b : α), a ≤ b → b ∈ s
-- Mathlib.Algebra.Module.Lattice
/-- An `R`-submodule `M` of `V` is a lattice if it is finitely generated
and spans `V` as an `A`-module.

Note 1: `A` is marked as an `outParam` here. In practice this should not cause issues, since
`R` and `A` are fixed, where typically `A` is the fraction field of `R`.

Note 2: In the case `R = ℤ` and `A = K` a field, there is also `IsZLattice` where the finitely
generated condition is replaced by having the discrete topology.  -/
Submodule.IsLattice : {R : Type u_1} →
  [inst : CommRing R] →
    (A : outParam (Type u_2)) →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra R A] →
          {V : Type u_3} →
            [inst_3 : AddCommMonoid V] →
              [inst_4 : Module R V] →
                [inst_5 : Module A V] → [IsScalarTower R A V] → [IsScalarTower R A V] → Submodule R V → Prop
-- Mathlib.Order.Hom.Lattice
SupHom.instFunLike : {α : Type u_2} → {β : Type u_3} → [inst : Max α] → [inst_1 : Max β] → FunLike (SupHom α β) α β
-- Mathlib.Data.Nat.Bitwise
Nat.shiftLeft_lt : ∀ {x n m : ℕ}, x < 2 ^ n → x <<< m < 2 ^ (n + m)
-- Batteries.Data.AssocList
Batteries.AssocList.instLawfulBEq : ∀ {α : Type u_1} {β : Type u_2} [inst : BEq α] [LawfulBEq α] [inst_2 : BEq β] [LawfulBEq β],
  LawfulBEq (Batteries.AssocList α β)
-- Mathlib.FieldTheory.IntermediateField.Algebraic
/-- If `L/K` is algebraic, the `K`-subalgebras of `L` are all fields.  -/
subalgebraEquivIntermediateField : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] → [inst_2 : Algebra K L] → [Algebra.IsAlgebraic K L] → Subalgebra K L ≃o IntermediateField K L
-- Mathlib.RingTheory.Valuation.RamificationGroup
/-- The inertia subgroup defined as the kernel of the group homomorphism from
the decomposition subgroup to the group of automorphisms of the residue field of `A`.  -/
ValuationSubring.inertiaSubgroup : (K : Type u_1) →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] → (A : ValuationSubring L) → Subgroup ↥(ValuationSubring.decompositionSubgroup K A)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_le_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → ∀ {k : α}, k ∈ t → (compare t.minKey! k).isLE = true
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.mapNatTrans_τ₁ : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C)
  {F G : CategoryTheory.Functor C D} [inst_4 : F.PreservesZeroMorphisms] [inst_5 : G.PreservesZeroMorphisms]
  (τ : F ⟶ G), (S.mapNatTrans τ).τ₁ = τ.app S.X₁
-- Lean.Declaration
Lean.mkInductiveDeclEs : List Lean.Name → ℕ → List Lean.InductiveType → Bool → Lean.Declaration
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.arg_exp : ∀ {x : ℝ}, -Real.pi < x → x ≤ Real.pi → (↑(Circle.exp x)).arg = x
-- Batteries.Data.Nat.Basic
/-- Simple diagonal recursor for `Nat`
 -/
Nat.recDiagAux : {motive : ℕ → ℕ → Sort u_1} →
  ((n : ℕ) → motive 0 n) →
    ((m : ℕ) → motive m 0) → ((m n : ℕ) → motive m n → motive (m + 1) (n + 1)) → (m n : ℕ) → motive m n
-- Mathlib.Order.Sublocale
Sublocale.carrier.instOrderTop : {X : Type u_1} → [inst : Order.Frame X] → {S : Sublocale X} → OrderTop ↥S
-- Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
CategoryTheory.Precoverage.ZeroHypercover.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C}
  [J.toGrothendieck.Subcanonical] {X Y : C} (𝒰 : J.ZeroHypercover X) {f g : X ⟶ Y},
  (∀ (i : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (𝒰.f i) f = CategoryTheory.CategoryStruct.comp (𝒰.f i) g) → f = g
-- Init.Data.Array.Lemmas
/-- Variant of `foldr_cons_eq_append` specialized to `f = id`.  -/
Array.foldr_cons_eq_append' : ∀ {α : Type u_1} {start : ℕ} {as : Array α} {bs : List α},
  start = as.size → Array.foldr List.cons bs as start = as.toList ++ bs
-- Mathlib.NumberTheory.Transcendental.Liouville.Measure
/-- **Alias** of `setOfPred_liouvilleWith_subset_aux`. -/
setOf_liouvilleWith_subset_aux : {x | ∃ p > 2, LiouvilleWith p x} ⊆
  ⋃ m,
    (fun x => x + ↑m) ⁻¹'
      ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in Filter.atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}
-- Mathlib.RingTheory.PowerBasis
PowerBasis.dim_le_degree_of_root : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] (h : PowerBasis A S)
  {p : Polynomial A}, p ≠ 0 → (Polynomial.aeval h.gen) p = 0 → ↑h.dim ≤ p.degree
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.map_zero_eq_bot : ∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) {N : Type u_5} [inst_1 : AddGroup N], AddSubgroup.map 0 K = ⊥
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.eq_modMonomial_single : ∀ {R : Type u_2} [inst : CommSemiring R] [IsLeftCancelAdd R] {σ : Type u_3} {i : σ} {p q r : MvPolynomial σ R},
  p = MvPolynomial.X i * q + r → (∀ n ∈ r.support, n i = 0) → r = p.modMonomial fun₀ | i => 1
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.sqrt_nnrpow_two : ∀ {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] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A]
  [IsSemitopologicalRing A] [T2Space A] (a : A), autoParam (0 ≤ a) CFC.sqrt_nnrpow_two._auto_1 → CFC.sqrt (a ^ 2) = a
-- Mathlib.GroupTheory.Congruence.Defs
ConGen.Rel.below.of : ∀ {M : Type u_1} [inst : Mul M] {r : M → M → Prop} {motive : (a a_1 : M) → ConGen.Rel r a a_1 → Prop} (x y : M)
  (a : r x y), ConGen.Rel.below ⋯
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- The symbol `J(a | 0)` has the value `1`.  -/
jacobiSym.zero_right : ∀ (a : ℤ), jacobiSym a 0 = 1
-- Init.Data.BitVec.Lemmas
BitVec.getMsb_eq_getLsb : ∀ {w : ℕ} (x : BitVec w) (i : Fin w), x.getMsb i = x.getLsb ⟨w - 1 - ↑i, ⋯⟩
-- Mathlib.Analysis.Calculus.FDeriv.Basic
DifferentiableWithinAt.of_finite : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s : Set E} [T1Space E], s.Finite → DifferentiableWithinAt 𝕜 f s x
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.uliftFunctor_map : ∀ {x x_1 : CommMonCat} (f : x ⟶ x_1),
  CommMonCat.uliftFunctor.map f =
    CommMonCat.ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((CommMonCat.Hom.hom f).comp MulEquiv.ulift.toMonoidHom))
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.beth.eq_1 : ∀ (o : Ordinal.{u}), Cardinal.beth o = Cardinal.preBeth (Ordinal.omega0 + o)
-- Init.Data.Order.PackageFactories
/-- This structure contains all the data needed to create a `LinearOrderPackage α` instance.
Its fields are automatically provided if possible. For the detailed rules how the fields are
inferred, see `LinearOrderPackage.ofOrd`.
 -/
Std.Packages.LinearOrderOfOrdArgs : Type u → Type u
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.add_neg_mul : ∀ {w : ℕ} {x y : BitVec w}, ~~~(x + x * y) + 1#w = x * ~~~y
-- Aesop.Search.Main
Aesop.search : Lean.MVarId →
  optParam (Option Aesop.LocalRuleSet) none →
    optParam Aesop.Options { } →
      optParam Lean.Meta.Simp.Config { } →
        optParam (Option Lean.Term) none → optParam Aesop.Stats ∅ → Lean.MetaM (Array Lean.MVarId × Aesop.Stats)
-- Mathlib.RingTheory.RamificationInertia.Ramification
Ideal.ramificationIdx_eq_one_iff : ∀ {S : Type u_1} [inst : CommRing S] {q : Ideal S} {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R S]
  [inst_3 : q.IsPrime] [Algebra.EssFiniteType R S] [Algebra.IsIntegral R S]
  [PerfectField (Ideal.under R q).ResidueField], q.ramificationIdx R = 1 ↔ Algebra.IsUnramifiedAt R q
-- Mathlib.Algebra.GroupWithZero.Units.Basic
/-- An element of the unit group of a nonzero monoid with zero represented as an element
of the monoid is nonzero.  -/
Units.ne_zero : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [Nontrivial M₀] (u : M₀ˣ), ↑u ≠ 0
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α], m₁.WF → m₂.WF → ∀ {k : α} [inst_3 : Inhabited (β k)], k ∉ m₁ → (m₁ \ m₂).get! k = default
-- Mathlib.Topology.EMetricSpace.Lipschitz
LocallyLipschitz.eq_1 : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (f : α → β),
  LocallyLipschitz f = ∀ (x : α), ∃ K, ∃ t ∈ nhds x, LipschitzOnWith K f t
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.NormalExpr.brecOn.go : {motive : Mathlib.Tactic.Abel.NormalExpr → Sort u} →
  (t : Mathlib.Tactic.Abel.NormalExpr) →
    ((t : Mathlib.Tactic.Abel.NormalExpr) → Mathlib.Tactic.Abel.NormalExpr.below t → motive t) →
      motive t ×' Mathlib.Tactic.Abel.NormalExpr.below t
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false}, t.maxKey he ∈ t
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₂_app_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D}
  (μ : CategoryTheory.MonoidalCategory.curriedTensorPre F ⟶ CategoryTheory.MonoidalCategory.curriedTensorPost F)
  (X₁ X₂ X₃ : C),
  (((CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₂ μ).app X₁).app X₂).app X₃ =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X₁) ((μ.app X₂).app X₃)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
BorelSpace.mk : ∀ {α : Type u_6} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α], inst_1 = borel α → BorelSpace α
-- Std.Data.DHashMap.Raw
_private.Std.Data.DHashMap.Raw.0.Std.DHashMap.Raw.Const.insertManyIfNewUnit.eq_1 : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type w} [inst_2 : ForIn Id ρ α]
  (m : Std.DHashMap.Raw α fun x => Unit) (l : ρ),
  Std.DHashMap.Raw.Const.insertManyIfNewUnit m l =
    if h : 0 < m.buckets.size then ↑↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit ⟨m, h⟩ l) else m
-- Init.Data.Fin.Basic
/-- Adds a natural number to a `Fin`, increasing the bound.

This is a generalization of `Fin.succ`.

`Fin.addNat` is a version of this function that takes its `Nat` parameter second.

Examples:
* `Fin.natAdd 3 (5 : Fin 8) = (8 : Fin 11)`
* `Fin.natAdd 1 (0 : Fin 8) = (1 : Fin 9)`
* `Fin.natAdd 1 (2 : Fin 8) = (3 : Fin 9)`
 -/
Fin.natAdd : {m : ℕ} → (n : ℕ) → Fin m → Fin (n + m)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyPrepareParams.mk.inj : ∀ {toTextDocumentPositionParams toTextDocumentPositionParams_1 : Lean.Lsp.TextDocumentPositionParams},
  { toTextDocumentPositionParams := toTextDocumentPositionParams } =
      { toTextDocumentPositionParams := toTextDocumentPositionParams_1 } →
    toTextDocumentPositionParams = toTextDocumentPositionParams_1
-- Init.Data.Int.LemmasAux
Int.mul_le_mul_of_le_of_le_of_nonneg_of_nonneg : ∀ {a b c d : ℤ}, a ≤ c → b ≤ d → 0 ≤ b → 0 ≤ c → a * b ≤ c * d
-- Mathlib.Order.WellFoundedSet
Set.PartiallyWellOrderedOn.mono : ∀ {α : Type u_2} {r : α → α → Prop} {s t : Set α}, t.PartiallyWellOrderedOn r → s ⊆ t → s.PartiallyWellOrderedOn r
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonLeanFileProgressParams : Lean.FromJson Lean.Lsp.LeanFileProgressParams
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
MulRingNorm.mk.sizeOf_spec : ∀ {R : Type u_2} [inst : NonAssocRing R] [inst_1 : SizeOf R] (toMulRingSeminorm : MulRingSeminorm R)
  (eq_zero_of_map_eq_zero' : ∀ (x : R), toMulRingSeminorm.toFun x = 0 → x = 0),
  sizeOf { toMulRingSeminorm := toMulRingSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' } =
    1 + sizeOf toMulRingSeminorm
-- Mathlib.Algebra.Lie.Weights.Killing
LieSubalgebra.root.congr_simp : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra],
  LieSubalgebra.root = LieSubalgebra.root
-- Lean.Elab.Match
Lean.Elab.Term.withPatternVars : {α : Type} →
  Array Lean.Elab.Term.PatternVar →
    (Array Lean.Elab.Term.PatternVarDecl → Lean.Elab.TermElabM α) → Lean.Elab.TermElabM α
-- Mathlib.Data.List.Cycle
_private.Mathlib.Data.List.Cycle.0.List.prev.match_1.splitter : {α : Type u_1} →
  (motive : (x : List α) → (x_1 : α) → x_1 ∈ x → Sort u_2) →
    (x : List α) →
      (x_1 : α) →
        (x_2 : x_1 ∈ x) →
          ((x : α) → (h : x ∈ []) → motive [] x h) →
            ((y x : α) → (x_3 : x ∈ [y]) → motive [y] x x_3) →
              ((y z : α) → (xs : List α) → (x : α) → (h : x ∈ y :: z :: xs) → motive (y :: z :: xs) x h) →
                motive x x_1 x_2
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.isoOfHom_hom_inv_id : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : L.IsLocalization W] {X Y : C} (f : X ⟶ Y) (hf : W f),
  CategoryTheory.CategoryStruct.comp (L.map f) (CategoryTheory.Localization.isoOfHom L W f hf).inv =
    CategoryTheory.CategoryStruct.id (L.obj X)
-- Mathlib.Analysis.Asymptotics.LinearGrowth
Monotone.linearGrowthSup_comp_mul : ∀ {u : ℕ → EReal} {m : ℕ},
  Monotone u → m ≠ 0 → (LinearGrowth.linearGrowthSup fun n => u (m * n)) = ↑m * LinearGrowth.linearGrowthSup u
-- Mathlib.Order.SupIndep
sSupIndep_empty : ∀ {α : Type u_1} [inst : CompleteLattice α], sSupIndep ∅
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.unit_actionHomRight : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {x y : D} (f : x ⟶ y),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight
      (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso x).hom
      (CategoryTheory.CategoryStruct.comp f
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso y).inv)
-- Mathlib.Analysis.InnerProductSpace.Subspace
OrthogonalFamily.inner_right_dfinsupp : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {G : ι → Type u_5} [inst_3 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E},
  OrthogonalFamily 𝕜 G V →
    ∀ [inst_5 : (i : ι) → (x : G i) → Decidable (x ≠ 0)] [inst_6 : DecidableEq ι] (l : DirectSum ι fun i => G i) (i : ι)
      (v : G i), inner 𝕜 ((V i) v) (DFinsupp.sum l fun j => ⇑(V j)) = inner 𝕜 v (l i)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_map : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β} [LawfulBEq α]
  {f : α → β → γ} {k : α},
  Std.DHashMap.Const.get? (Std.DHashMap.map f m) k = Option.map (f k) (Std.DHashMap.Const.get? m k)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_add_of_lt : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f g : MvPolynomial σ R},
  m.toSyn (m.degree g) < m.toSyn (m.degree f) → m.degree (f + g) = m.degree f
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintInfo.mk : String.Pos.Raw →
  Lean.Elab.InlayHintLabel →
    Option Lean.Elab.InlayHintKind →
      Array Lean.Elab.InlayHintTextEdit → Option String → Bool → Bool → Lean.Elab.InlayHintInfo