mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Bounds.Lattice
lowerBounds_iUnion : ∀ {α : Type u_1} [inst : Preorder α] {ι : Sort u_2} {s : ι → Set α}, lowerBounds (⋃ i, s i) = ⋂ i, lowerBounds (s i)
-- Mathlib.Algebra.Ring.Defs
add_sq' : ∀ {α : Type u} [inst : CommSemiring α] (a b : α), (a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * a * b
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Array
Array.length_iterFromIdxM : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} [LawfulMonad m] {array : Array β} {pos : ℕ},
  (array.iterFromIdxM m pos).length = pure { down := array.size - pos }
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.BuilderOption.transparency.inj : ∀ {md : Lean.Meta.TransparencyMode} {alsoForIndex : Bool} {md_1 : Lean.Meta.TransparencyMode} {alsoForIndex_1 : Bool},
  Aesop.Frontend.BuilderOption.transparency md alsoForIndex =
      Aesop.Frontend.BuilderOption.transparency md_1 alsoForIndex_1 →
    md = md_1 ∧ alsoForIndex = alsoForIndex_1
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron.triangle_obj₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃), h.triangle.obj₂ = Z₁₃
-- Mathlib.Data.Finsupp.Single
Finsupp.single_apply_mem : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a : α} {b : M} (x : α), (fun₀ | a => b) x ∈ {0, b}
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.coeff_cert : Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → ℕ → Bool
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- The inner product of a linear combination of a set of orthonormal vectors with one of those
vectors picks out the coefficient of that vector.  -/
Orthonormal.inner_right_finsupp : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {v : ι → E},
  Orthonormal 𝕜 v → ∀ (l : ι →₀ 𝕜) (i : ι), inner 𝕜 (v i) ((Finsupp.linearCombination 𝕜 v) l) = l i
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.instInhabited : Inhabited RingCat
-- Init.Data.Array.Monadic
/-- This lemma identifies monadic folds over lists of subtypes, where the function only depends on the value, not the proposition,
and simplifies these to the function directly taking the value.
 -/
Array.foldrM_subtype : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {start : ℕ} [inst : Monad m] [LawfulMonad m] {p : α → Prop}
  {xs : Array { x // p x }} {f : { x // p x } → β → m β} {g : α → β → m β} {x : β},
  (∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b) →
    start = xs.size → Array.foldrM f x xs start = Array.foldrM g x xs.unattach start
-- Mathlib.Combinatorics.Additive.FreimanHom
MulHomClass.isMulFreimanHom : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {A : Set α} {B : Set β}
  {n : ℕ} [inst_2 : FunLike F α β] [MulHomClass F α β] (f : F), Set.MapsTo (⇑f) A B → IsMulFreimanHom n A B ⇑f
-- Init.Tactics
/-- Close fixed-width `BitVec` and `Bool` goals by obtaining a proof from an external SAT solver and
verifying it inside Lean. The solvable goals are currently limited to
- the Lean equivalent of [`QF_BV`](https://smt-lib.org/logics-all.shtml#QF_BV)
- automatically splitting up `structure`s that contain information about `BitVec` or `Bool`
```lean
example : ∀ (a b : BitVec 64), (a &&& b) + (a ^^^ b) = a ||| b := by
  intros
  bv_decide
```

If `bv_decide` encounters an unknown definition it will be treated like an unconstrained `BitVec`
variable. Sometimes this enables solving goals despite not understanding the definition because
the precise properties of the definition do not matter in the specific proof.

If `bv_decide` fails to close a goal it provides a counter-example, containing assignments for all
terms that were considered as variables.

In order to avoid calling a SAT solver every time, the proof can be cached with `bv_decide?`.

If solving your problem relies inherently on using associativity or commutativity, consider enabling
the `bv.ac_nf` option.

Note: `bv_decide` trusts the correctness of the code generator and adds a axioms asserting its result.

Note: include `import Std.Tactic.BVDecide`
 -/
Lean.Parser.Tactic.bvDecideMacro : Lean.ParserDescr
-- Mathlib.CategoryTheory.Join.Sum
CategoryTheory.Join.instFaithfulSumFromSum : ∀ (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], (CategoryTheory.Join.fromSum C D).Faithful
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.HasSubst.substInvOfIsUnit : ∀ {R : Type u_2} [inst : CommRing R] (P : PowerSeries R) (hP' : IsUnit ((PowerSeries.coeff 1) P)),
  PowerSeries.HasSubst (P.substInvOfIsUnit hP')
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
ENNReal.tendsto_rpow_at_top : ∀ {y : ℝ}, 0 < y → Filter.Tendsto (fun x => x ^ y) (nhds ⊤) (nhds ⊤)
-- Mathlib.Data.List.Sort
/-- **Alias** of the forward direction of `List.sortedLE_iff_monotone_get`. -/
List.SortedLE.monotone_get : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedLE → Monotone l.get
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.optionEquivLeft_X_none : ∀ (R : Type u) (S₁ : Type v) [inst : CommSemiring R],
  (MvPolynomial.optionEquivLeft R S₁) (MvPolynomial.X none) = Polynomial.X
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.mul_sub_left_right_iff : ∀ {R : Type u_1} [inst : CommRing R] {x y z : R}, IsRelPrime x (x * z - y) ↔ IsRelPrime x y
-- Lean.Parser.Command
Lean.Parser.Command.set_option.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- A normal monomorphism is a morphism which is the kernel of some morphism.  -/
CategoryTheory.NormalMono.isLimit : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {X Y : C} →
      {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} →
        {f : X ⟶ Y} →
          [self : CategoryTheory.NormalMono f] →
            CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι f ⋯)
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveElabDescr.mk.sizeOf_spec : ∀ (mkInductiveView : Lean.Elab.Modifiers → Lean.Syntax → Lean.Elab.TermElabM Lean.Elab.Command.InductiveElabStep1),
  sizeOf { mkInductiveView := mkInductiveView } = 1
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivAtFilter_iff_isLittleO : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {L : Filter (𝕜 × 𝕜)},
  HasDerivAtFilter f f' L ↔ (fun p => f p.1 - f p.2 - (p.1 - p.2) • f') =o[L] fun p => p.1 - p.2
-- Init.Data.List.Basic
List.getLast?_nil : ∀ {α : Type u}, [].getLast? = none
-- Lean.Server.FileWorker.InlayHints
Lean.Server.FileWorker.InlayHintState.isFirstRequestAfterEdit : Lean.Server.FileWorker.InlayHintState → Bool
-- Mathlib.Algebra.Group.Idempotent
IsIdempotentElem.mul_mul_self : ∀ {M : Type u_4} [inst : Semigroup M] {x : M}, IsIdempotentElem x → ∀ (y : M), y * x * x = y * x
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Stats.maxDepth : Lean.PersistentHashMap.Stats → ℕ
-- Std.Data.TreeMap.Raw.Basic
Std.TreeMap.Raw.instBEq : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [BEq β] → BEq (Std.TreeMap.Raw α β cmp)
-- Mathlib.Topology.Order.HullKernel
PrimitiveSpectrum.hull_sSup : ∀ {α : Type u_1} [inst : CompleteLattice α] {T : Set α} (S : Set α),
  PrimitiveSpectrum.hull T (sSup S) = ⋂₀ {x | ∃ a ∈ S, PrimitiveSpectrum.hull T a = x}
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
_private.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.0.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze.analyzeProj : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit
-- Mathlib.Analysis.Asymptotics.ExpGrowth
Monotone.expGrowthSup_comp : ∀ {u : ℕ → ENNReal} {v : ℕ → ℕ} {a : EReal},
  Monotone u →
    Filter.Tendsto (fun n => ↑(v n) / ↑n) Filter.atTop (nhds a) →
      a ≠ 0 → a ≠ ⊤ → ExpGrowth.expGrowthSup (u ∘ v) = a * ExpGrowth.expGrowthSup u
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- **Alias** of `AddMonoidHom.domRestrictHomKerEquiv`.

---

The `AddEquiv` between the kernel of the restriction map to a normal subgroup `H` of homomorphisms
of type `G →+ A` and the group of homomorphisms `G ⧸ H →+ A`.
 -/
AddMonoidHom.restrictHomKerEquiv : {G : Type u} →
  [inst : AddGroup G] →
    (A : Type u_1) →
      [inst_1 : AddCommGroup A] →
        (H : AddSubgroup G) → [inst_2 : H.Normal] → ↥(AddMonoidHom.domRestrictHom H A).ker ≃+ (G ⧸ H →+ A)
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
CategoryTheory.ObjectProperty.instIsClosedUnderKernelsOfIsClosedUnderSubobjects : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderSubobjects], P.IsClosedUnderKernels
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.coweightEquiv_inv : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (g : P.Aut),
  RootPairing.Equiv.coweightEquiv P P g⁻¹ = (RootPairing.Equiv.coweightEquiv P P g)⁻¹
-- Mathlib.Tactic.ProdAssoc
/-- The components of an iterated product, presented as a `ProdTree`.  -/
Lean.Expr.ProdTree.components : Lean.Expr.ProdTree → List Lean.Expr
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveElabStep2.mk.inj : ∀ {ctors : List Lean.Constructor} {collectUsedFVars : StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM Unit}
  {collectExtraHeaderLMVars : StateRefT' IO.RealWorld Lean.CollectLevelMVars.State Lean.MetaM Unit}
  {checkUniverses : ℕ → Lean.Level → Lean.Elab.TermElabM Unit} {finalizeTermElab : Lean.Elab.TermElabM Unit}
  {prefinalize :
    List Lean.Name →
      Array Lean.Expr → (Lean.Expr → Lean.MetaM Lean.Expr) → Lean.Elab.TermElabM Lean.Elab.Command.InductiveElabStep3}
  {ctors_1 : List Lean.Constructor}
  {collectUsedFVars_1 : StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM Unit}
  {collectExtraHeaderLMVars_1 : StateRefT' IO.RealWorld Lean.CollectLevelMVars.State Lean.MetaM Unit}
  {checkUniverses_1 : ℕ → Lean.Level → Lean.Elab.TermElabM Unit} {finalizeTermElab_1 : Lean.Elab.TermElabM Unit}
  {prefinalize_1 :
    List Lean.Name →
      Array Lean.Expr → (Lean.Expr → Lean.MetaM Lean.Expr) → Lean.Elab.TermElabM Lean.Elab.Command.InductiveElabStep3},
  { ctors := ctors, collectUsedFVars := collectUsedFVars, collectExtraHeaderLMVars := collectExtraHeaderLMVars,
        checkUniverses := checkUniverses, finalizeTermElab := finalizeTermElab, prefinalize := prefinalize } =
      { ctors := ctors_1, collectUsedFVars := collectUsedFVars_1,
        collectExtraHeaderLMVars := collectExtraHeaderLMVars_1, checkUniverses := checkUniverses_1,
        finalizeTermElab := finalizeTermElab_1, prefinalize := prefinalize_1 } →
    ctors = ctors_1 ∧
      collectUsedFVars = collectUsedFVars_1 ∧
        collectExtraHeaderLMVars = collectExtraHeaderLMVars_1 ∧
          checkUniverses = checkUniverses_1 ∧ finalizeTermElab = finalizeTermElab_1 ∧ prefinalize = prefinalize_1
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.rightUnitor_monoidal_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X₁ X₂ : C) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.rightUnitor X₁).hom
        (CategoryTheory.MonoidalCategoryStruct.rightUnitor X₂).hom)
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.tensorμ X₁ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X₂
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.rightUnitor
              (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)).hom
          h))
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.nontrivial_iff : ∀ {M : Type u_1} [inst : MulOneClass M], Nontrivial (Submonoid M) ↔ Nontrivial M
-- Init.Grind.Norm
Lean.Grind.Nat.pow_one : ∀ (a : ℕ), a ^ 1 = a
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.degreewiseEpiWithInjectiveKernel_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] (n : ℤ),
  CochainComplex.degreewiseEpiWithInjectiveKernel (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.π✝ f n)
-- Mathlib.Algebra.Lie.Basis.Base
LieAlgebra.Basis.cartanMatrix_base_eq : ∀ {ι : Type u_1} {K : Type u_2} {L : Type u_3} [inst : Fintype ι] [inst_1 : Field K] [inst_2 : CharZero K]
  [inst_3 : LieRing L] [inst_4 : LieAlgebra K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L}
  (b : LieAlgebra.Basis ι H) [inst_6 : LieModule.IsTriangularizable K (↥H) L] [inst_7 : LieAlgebra.IsKilling K L],
  b.base.cartanMatrix = (Matrix.reindex b.baseSupportEquiv b.baseSupportEquiv) b.A
-- Batteries.Data.Array.Scan
Array.scanlM_map : ∀ {m : Type u_1 → Type u_2} {α₁ : Type u_3} {α₂ : Type u_4} {β : Type u_1} {init : β} [inst : Monad m] [LawfulMonad m]
  {f : α₁ → α₂} {g : β → α₂ → m β} {as : Array α₁},
  Array.scanlM g init (Array.map f as) = Array.scanlM (fun x1 x2 => g x1 (f x2)) init as
-- Mathlib.Algebra.Group.Submonoid.BigOperators
AddSubmonoid.coe_list_sum : ∀ {M : Type u_1} [inst : AddMonoid M] (s : AddSubmonoid M) (l : List ↥s), ↑l.sum = (List.map Subtype.val l).sum
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- a section of `S.g`  -/
CategoryTheory.ShortComplex.Splitting.s : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] → {S : CategoryTheory.ShortComplex C} → S.Splitting → (S.X₃ ⟶ S.X₂)
-- Lean.Parser.Term.Basic
Lean.Parser.Term.optEllipsis.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_mono_measure : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_2 : PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E]
  [OrderClosedTopology E] {f : α → E} {ν : MeasureTheory.Measure α},
  μ ≤ ν → 0 ≤ᵐ[ν] f → MeasureTheory.Integrable f ν → ∫ (a : α), f a ∂μ ≤ ∫ (a : α), f a ∂ν
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
CliffordAlgebra.even.lift.aux_algebraMap : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {A : Type u_3} [inst_3 : Ring A] [inst_4 : Algebra R A] (f : CliffordAlgebra.EvenHom Q A)
  (r : R), (CliffordAlgebra.even.lift.aux f) ((algebraMap R ↥(CliffordAlgebra.even Q)) r) = (algebraMap R A) r
-- Mathlib.LinearAlgebra.TensorProduct.Tower
LinearEquiv.baseChange_pow : ∀ (R : Type u_1) (A : Type u_2) (M : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (f : M ≃ₗ[R] M) (n : ℕ),
  LinearEquiv.baseChange R A M M (f ^ n) = LinearEquiv.baseChange R A M M f ^ n
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey!_le_maxKey!_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.isEmpty = false → ∀ {k : α} {v : β k}, (cmp t.maxKey! (t.insert k v).maxKey!).isLE = true
-- Mathlib.Topology.Inseparable
SpecializingMap.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
  SpecializingMap f = Relation.Fibration (flip fun x1 x2 => x1 ⤳ x2) (flip fun x1 x2 => x1 ⤳ x2) f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_union!_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (contains_eq_false : Std.DTreeMap.Internal.Impl.contains k m₁ = false)
  {h' : Std.DTreeMap.Internal.Impl.contains k (m₁.union! m₂) = true}, (m₁.union! m₂).getKey k h' = m₂.getKey k ⋯
-- Lean.SubExpr
Lean.SubExpr.Pos.instToString : ToString Lean.SubExpr.Pos
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Compose a `SMulZeroClass` with a function, with scalar multiplication `f r' • m`.
See note [reducible non-instances].  -/
SMulZeroClass.compFun : {M : Type u_1} → {N : Type u_6} → (A : Type u_7) → [inst : Zero A] → [SMulZeroClass M A] → (N → M) → SMulZeroClass N A
-- Mathlib.ModelTheory.Definability
/-- TermDefinable is transitive. If f is TermDefinable in a structure S on L, and all of the
functions' realizations on S are TermDefinable on a structure T on L', then f is
TermDefinable on T in L'.  -/
Set.TermDefinable.trans : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} {L' : FirstOrder.Language} [inst : L.Structure M]
  [inst_1 : L'.Structure M] {β : Type u_1} {f : (β → M) → M},
  A.TermDefinable L f →
    (∀ {n : ℕ} (g : (L.withConstants ↑A).Functions n),
        A.TermDefinable L' fun v => FirstOrder.Language.Term.realize v g.term) →
      A.TermDefinable L' f
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.comap_comap : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P] (S : AddSubmonoid P) (g : N →+ P) (f : M →+ N),
  AddSubmonoid.comap f (AddSubmonoid.comap g S) = AddSubmonoid.comap (g.comp f) S
-- Init.Data.String.Search
/-- Checks whether the string can be interpreted as the decimal representation of a natural number.

A slice can be interpreted as a decimal natural number if it is not empty and all the characters in
it are digits.

Use `toNat?` or
`toNat!` to convert such a slice to a natural number.

Examples:

* `"".isNat = false`

* `"0".isNat = true`

* `"5".isNat = true`

* `"05".isNat = true`

* `"587".isNat = true`

* `"-587".isNat = false`

* `" 5".isNat = false`

* `"2+3".isNat = false`

* `"0xff".isNat = false`
 -/
String.isNat : String → Bool
-- Mathlib.RingTheory.Valuation.ValuationSubring
Valuation.isEquiv_valuation_valuationSubring : ∀ {K : Type u} [inst : Field K] {Γ : Type u_1} [inst_1 : LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ),
  v.IsEquiv v.valuationSubring.valuation
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
/-- If `I` is an ideal in a `ℚ`-algebra `A`, then `I` admits a unique divided power structure,
given by `dpow n x = x ^ n / n!`.  -/
DividedPowers.RatAlgebra.dividedPowers : {R : Type u_1} →
  [inst : CommSemiring R] → (I : Ideal R) → [DecidablePred fun x => x ∈ I] → [Algebra ℚ R] → DividedPowers I
-- Mathlib.Algebra.Order.Group.Synonym
ofLex_inv : ∀ {α : Type u_1} [inst : Inv α] (a : Lex α), ofLex a⁻¹ = (ofLex a)⁻¹
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Box.splitLower_def : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} [inst : DecidableEq ι] {i : ι} {x : ℝ}
  (h : x ∈ Set.Ioo (I.lower i) (I.upper i)) (h' : optParam (∀ (j : ι), I.lower j < Function.update I.upper i x j) ⋯),
  I.splitLower i x = ↑{ lower := I.lower, upper := Function.update I.upper i x, lower_lt_upper := h' }
-- Init.Data.BitVec.Lemmas
BitVec.rotateRightAux.eq_1 : ∀ {w : ℕ} (x : BitVec w) (n : ℕ), x.rotateRightAux n = x >>> n ||| x <<< (w - n)
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A weighted sum over `{x ∈ s | pred x}` equals one over `s` if all the weights at indices in `s`
not satisfying `pred` are zero.  -/
Finset.weightedVSub_filter_of_ne : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) {pred : ι → Prop}
  [inst_3 : DecidablePred pred],
  (∀ i ∈ s, w i ≠ 0 → pred i) → ({x ∈ s | pred x}.weightedVSub p) w = (s.weightedVSub p) w
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mapIso_inverse_map_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T T' : D} {S : CategoryTheory.Functor C D} (i : T ≅ T')
  {Y X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T')} (f : Y ⟶ X),
  ((CategoryTheory.CostructuredArrow.mapIso i).inverse.map f).right = CategoryTheory.CategoryStruct.id Y.right
-- Mathlib.NumberTheory.MahlerMeasure
_private.Mathlib.NumberTheory.MahlerMeasure.0.Polynomial.card_mahlerMeasure : ∀ (n : ℕ) (B : NNReal),
  {p | p.natDegree ≤ n ∧ (Polynomial.map (Int.castRingHom ℂ) p).mahlerMeasure ≤ ↑B}.Finite ∧
    {p | p.natDegree ≤ n ∧ (Polynomial.map (Int.castRingHom ℂ) p).mahlerMeasure ≤ ↑B}.ncard ≤
      ∏ i, (2 * ⌊↑(n.choose ↑i) * B⌋₊ + 1)
-- Mathlib.Order.Filter.Tendsto
Filter.EventuallyEq.comp_tendsto : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} {f f' : α → β},
  f =ᶠ[l] f' → ∀ {g : γ → α} {lc : Filter γ}, Filter.Tendsto g lc l → f ∘ g =ᶠ[lc] f' ∘ g
-- Mathlib.Algebra.Group.Fin.Tuple
Fin.insertNth_div : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} [inst : (j : Fin (n + 1)) → Div (α j)] (i : Fin (n + 1)) (x y : α i)
  (p q : (j : Fin n) → α (i.succAbove j)), i.insertNth (x / y) (p / q) = i.insertNth x p / i.insertNth y q
-- Mathlib.Algebra.Category.Grp.Biproducts
AddCommGrpCat.HasLimit.lift_hom_apply : ∀ {J : Type w} (f : J → AddCommGrpCat) (s : CategoryTheory.Limits.Fan f) (x : ↑s.1) (j : J),
  (AddCommGrpCat.Hom.hom (AddCommGrpCat.HasLimit.lift f s)) x j =
    (CategoryTheory.ConcreteCategory.hom (s.π.app { as := j })) x
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.Functor.mapCommMon_id_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommMon C),
  CategoryTheory.MonObj.one =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) CategoryTheory.MonObj.one
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.degree_gcd_le_left : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] {p : Polynomial R},
  p ≠ 0 → ∀ (q : Polynomial R), (gcd p q).degree ≤ p.degree
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.IsImmersion.instToImage : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsImmersion f],
  AlgebraicGeometry.IsImmersion (AlgebraicGeometry.Scheme.Hom.toImage f)
-- Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Unitary.toLinearMap_mulRight : ∀ {R : Type u_1} {A : Type u_2} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : CStarRing A] [inst_3 : Ring R]
  [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] (u : ↥(unitary A)),
  ↑(Unitary.mulRight R u).toLinearEquiv = LinearMap.mulRight R ↑u