mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec_fromSpecStalk_assoc : ∀ {X : AlgebraicGeometry.Scheme} {R : CommRingCat} [inst : IsLocalRing ↑R] {x : ↥X} (f : X.presheaf.stalk x ⟶ R)
  [inst_1 : IsLocalHom (CommRingCat.Hom.hom f)] (U : X.Opens)
  (hU :
    (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map f) (X.fromSpecStalk x))
        (IsLocalRing.closedPoint ↑R) ∈
      U)
  {Z : CommRingCat} (h : R ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (X.presheaf.germ U
        ((CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map f) (X.fromSpecStalk x))
          (IsLocalRing.closedPoint ↑R))
        hU)
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Scheme.stalkClosedPointTo
          (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map f) (X.fromSpecStalk x)))
        h) =
    CategoryTheory.CategoryStruct.comp (X.presheaf.germ U x ⋯) (CategoryTheory.CategoryStruct.comp f h)
-- Init.Data.String.Termination
/-- Use `termination_by pos.down` to signify that in a recursive call, the parameter `pos` is
expected to decrease.  -/
String.Pos.down : {s : String} → s.Pos → String.Pos.Down s
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The projection map to the first component of the product.  -/
CategoryTheory.Limits.prod.fst : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → [inst_1 : CategoryTheory.Limits.HasBinaryProduct X Y] → X ⨯ Y ⟶ X
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.support_scaleRoots_le : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) (s : R), (p.scaleRoots s).support ⊆ p.support
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.smul_map_inv_div_map_inv_of_isMulCocycle₂ : ∀ {G : Type u_1} {M : Type u_2} [inst : Group G] [inst_1 : CommGroup M] [inst_2 : MulAction G M] {f : G × G → M},
  groupCohomology.IsMulCocycle₂ f → ∀ (g : G), g • f (g⁻¹, g) / f (g, g⁻¹) = f (1, 1) / f (g, 1)
-- Plausible.Shrinkable
Plausible.String.shrinkable : Plausible.Shrinkable String
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- Eta-expanded form of `MeasureTheory.StronglyMeasurable.sup` -/
MeasureTheory.StronglyMeasurable.fun_sup : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Max β]
  [ContinuousSup β],
  MeasureTheory.StronglyMeasurable f →
    MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable fun i => f i ⊔ g i
-- Mathlib.Order.Heyting.Hom
/-- `BiheytingHomClass F α β` states that `F` is a type of bi-Heyting homomorphisms.

You should extend this class when you extend `BiheytingHom`.  -/
BiheytingHomClass : (F : Type u_6) → (α : Type u_7) → (β : Type u_8) → [BiheytingAlgebra α] → [BiheytingAlgebra β] → [FunLike F α β] → Prop
-- Init.Prelude
instHShiftRightOfShiftRight : {α : Type u_1} → [ShiftRight α] → HShiftRight α α α
-- Batteries.Data.Stream
Std.List.stream_take_eq_take_drop : ∀ {α : Type u_1} {n : ℕ} (l : List α), Std.Stream.take l n = (List.take n l, List.drop n l)
-- Mathlib.Computability.EpsilonNFA
εNFA.evalFrom_singleton : ∀ {α : Type u} {σ : Type v} (M : εNFA α σ) (S : Set σ) (a : α), M.evalFrom S [a] = M.stepSet (M.εClosure S) a
-- Mathlib.Data.Fin.Tuple.Basic
Fin.contractNth_apply_of_lt : ∀ {n : ℕ} {α : Sort u_1} (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n),
  ↑k < ↑j → j.contractNth op g k = g k.castSucc
-- Mathlib.Combinatorics.Graph.Basic
Graph.IsLink.right_unique : ∀ {α : Type u_1} {β : Type u_2} {x y z : α} {e : β} {G : Graph α β}, G.IsLink e x y → G.IsLink e x z → y = z
-- Mathlib.Data.Seq.Defs
Stream'.Seq.coeStream : {α : Type u} → Coe (Stream' α) (Stream'.Seq α)
-- Init.Prelude
/-- Constructs a new empty array with initial capacity `c`.
 -/
Array.emptyWithCapacity : {α : Type u} → ℕ → Array α
-- Init.Sym.Simp.SimprocDSL
/-- Recursive simplification (calls the full simplifier).  -/
Lean.Parser.Sym.Simp.self : Lean.ParserDescr
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegral_restrictScalars : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F}
  {γ : Path a b} {𝕝 : Type u_4} [inst_5 : RCLike 𝕝] [inst_6 : NormedSpace 𝕝 F] [inst_7 : NormedSpace 𝕝 E]
  [inst_8 : LinearMap.CompatibleSMul E F 𝕝 𝕜],
  ∫ᶜ (x : E) in γ, ContinuousLinearMap.restrictScalars 𝕝 (ω x) = ∫ᶜ (x : E) in γ, ω x
-- Mathlib.Algebra.GroupWithZero.Action.Defs
smul_inv₀ : ∀ {G₀ : Type u_4} {G₀' : Type u_5} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero G₀']
  [inst_2 : MulActionWithZero G₀ G₀'] [SMulCommClass G₀ G₀' G₀'] [IsScalarTower G₀ G₀' G₀'] (c : G₀) (x : G₀'),
  (c • x)⁻¹ = c⁻¹ • x⁻¹
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.equivFnOfDiscrete_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : DiscreteTopology α]
  (f : C(α, β)) (a : α), ContinuousMap.equivFnOfDiscrete f a = f a
-- Mathlib.Order.CompleteLattice.Basic
iSup_bot : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α], ⨆ x, ⊥ = ⊥
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
/-- Leading coefficient of powers  -/
MonomialOrder.leadingCoeff_pow_of_pow_leadingCoeff_ne_zero : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f : MvPolynomial σ R} {n : ℕ},
  m.leadingCoeff f ^ n ≠ 0 → m.leadingCoeff (f ^ n) = m.leadingCoeff f ^ n
-- Std.Data.TreeMap.Basic
/-- Returns an array of all keys present in the tree map in ascending  order.  -/
Std.TreeMap.keysArray : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → Array α
-- Lean.DocString.Types
Lean.Doc.Block.concat.sizeOf_spec : ∀ {i : Type u} {b : Type v} [inst : SizeOf i] [inst_1 : SizeOf b] (content : Array (Lean.Doc.Block i b)),
  sizeOf (Lean.Doc.Block.concat content) = 1 + sizeOf content
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleIso_hom_app_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] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] {F₁ F₂ : CategoryTheory.Functor C D} (e : F₁ ≅ F₂) [inst_4 : F₁.CommShift ℤ]
  [inst_5 : F₂.CommShift ℤ] [inst_6 : CategoryTheory.NatTrans.CommShift e.hom ℤ]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  ((CategoryTheory.Functor.mapTriangleIso e).hom.app X).hom₂ = e.hom.app X.obj₂
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.sin_eq_zero_iff : ∀ {θ : ℂ}, Complex.sin θ = 0 ↔ ∃ k, θ = ↑k * ↑Real.pi
-- Mathlib.Algebra.Homology.Bifunctor
CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_toGradedObject : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  {I₁ : Type u_4} {I₂ : Type u_5} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (K₁ : HomologicalComplex C₁ c₁)
  (K₂ : HomologicalComplex C₂ c₂),
  (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).toGradedObject =
    ((CategoryTheory.GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X
-- Lean.Attributes
/-- This is used as the target for go-to-definition queries for simple attributes  -/
Lean.AttributeImplCore.ref : Lean.AttributeImplCore → Lean.Name
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.PreservesEpimorphisms.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  (∀ {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f], CategoryTheory.Epi (F.map f)) → F.PreservesEpimorphisms
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.nlt.inj : ∀ {lhs rhs : ℕ} {proof : Lean.Expr} {lhs_1 rhs_1 : ℕ} {proof_1 : Lean.Expr},
  Mathlib.Tactic.Order.AtomicFact.nlt lhs rhs proof = Mathlib.Tactic.Order.AtomicFact.nlt lhs_1 rhs_1 proof_1 →
    lhs = lhs_1 ∧ rhs = rhs_1 ∧ proof = proof_1
-- Init.WF
/-- The `wfParam` gadget is used internally during the construction of recursive functions by
wellfounded recursion, to keep track of the parameter for which the automatic introduction
of `List.attach` (or similar) is plausible.
 -/
wfParam : {α : Sort u} → α → α
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
HasDerivAt.exp : ∀ {f : ℝ → ℝ} {f' x : ℝ}, HasDerivAt f f' x → HasDerivAt (fun x => Real.exp (f x)) (Real.exp (f x) * f') x
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.throw_StateT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ε : Type u_1} {α σ : Type u} {e : ε} [inst : Std.Do.WP m ps]
  [inst_1 : Monad m] [inst_2 : MonadExceptOf ε m] (Q : Std.Do.PostCond α (Std.Do.PostShape.arg σ ps)),
  ⦃(Std.Do.wp (MonadLift.monadLift (MonadExceptOf.throw e))).apply Q⦄ MonadExceptOf.throw e ⦃Q⦄
-- Mathlib.Topology.UniformSpace.Basic
/-- Entourages are neighborhoods of the diagonal.  -/
nhdsSet_diagonal_le_uniformity : ∀ {α : Type ua} [inst : UniformSpace α], nhdsSet (Set.diagonal α) ≤ uniformity α
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
/-- The number of infinite complex places of the number field `K`.  -/
NumberField.InfinitePlace.nrComplexPlaces : (K : Type u_1) → [inst : Field K] → [NumberField K] → ℕ
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.curryFinFinset_apply_const : ∀ {𝕜 : Type u} {n : ℕ} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] [inst_3 : NormedAddCommGroup G'] [inst_4 : NormedSpace 𝕜 G'] {k l : ℕ} {s : Finset (Fin n)}
  (hk : s.card = k) (hl : sᶜ.card = l) (f : G [×n]→L[𝕜] G') (x y : G),
  ((((ContinuousMultilinearMap.curryFinFinset 𝕜 G G' hk hl) f) fun x_1 => x) fun x => y) =
    f (s.piecewise (fun x_1 => x) fun x => y)
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. Returns true if the given cut returns `eq` for something in the RBSet.  -/
RBTree.RBSet.containsP : {α : Type u_1} → {cmp : α → α → Ordering} → RBTree.RBSet α cmp → (α → Ordering) → Bool
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.forMUncurried_eq_forM_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {m : Type w → Type w'} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [inst : Monad m] [LawfulMonad m] {f : α × β → m PUnit.{w + 1}},
  Std.DTreeMap.Raw.Const.forMUncurried f t = Array.forM f (Std.DTreeMap.Raw.Const.toArray t)
-- Mathlib.RingTheory.Polynomial.Basic
/-- `R[X]` is never a field for any ring `R`.  -/
Polynomial.not_isField : ∀ (R : Type u) [inst : Ring R], ¬IsField (Polynomial R)
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.coeff_smul : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] {V : Type u_8} [inst_1 : Zero V] [inst_2 : SMulZeroClass R V]
  {r : R} {x : HahnSeries Γ V} {a : Γ}, (r • x).coeff a = r • x.coeff a
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int64.reduceOfInt : Lean.Meta.Simp.DSimproc
-- Mathlib.Topology.NhdsWithin
mem_nhdsSet : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : Set α}, s ∈ nhdsSet t ↔ ∃ u ⊆ s, IsOpen u ∧ t ⊆ u
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.sectR_apply : ∀ {α : Type u_1} (a : α) (β : Type u_2) (b : β), (Function.Embedding.sectR a β) b = (a, b)
-- Mathlib.Logic.Basic
exists_apply_eq_apply3 : ∀ {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} {δ : Sort u_6} {f : α → β → γ → δ} {a : α} {b : β} {c : γ},
  ∃ x y z, f x y z = f a b c
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.tmulEquiv.eq_1 : ∀ {ι : Type u_1} {ι₂ : Type u_2} (R : Type u_4) [inst : CommSemiring R] (M : Type u_8) [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M], PiTensorProduct.tmulEquiv R M = PiTensorProduct.tmulEquivDep R fun x => M
-- Std.Sat.AIG.RelabelNat
/-- We will find a `Nat` for every atom in the `AIG` that the `ofAIG` map was built from.
 -/
Std.Sat.AIG.RelabelNat.State.ofAIG_find_some : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {aig : Std.Sat.AIG α},
  ∀ a ∈ aig, ∃ n, (Std.Sat.AIG.RelabelNat.State.ofAIG aig)[a]? = some n
-- Mathlib.Analysis.Distribution.Support
Distribution.mem_dsupport_iff_forall_exists_ne : ∀ {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [inst : FunLike F α β] [inst_1 : TopologicalSpace α]
  [inst_2 : Zero β] [inst_3 : Zero V] {f : F → V} (x : α),
  x ∈ Distribution.dsupport f ↔ ∀ (s : Set α), x ∈ s → IsOpen s → ∃ u, tsupport ⇑u ⊆ s ∧ f u ≠ 0
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.ι_mapBifunctorComp₁₂MapObjIso_inv_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9}
  {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r)
  (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂)
  (X₃ : CategoryTheory.GradedObject I₃ C₃)
  [inst_5 : (((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
              (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
          X₃).HasMap
      ρ₁₂.q]
  [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
  [inst_7 :
    ((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj
          X₃).HasMap
      r]
  (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) {Z : C₄}
  (h_1 : CategoryTheory.GradedObject.mapTrifunctorMapObj (CategoryTheory.bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ j ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.GradedObject.mapBifunctorComp₁₂MapObjIso F₁₂ G ρ₁₂ X₁ X₂ X₃).inv j) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.ιMapTrifunctorMapObj (CategoryTheory.bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ i₁ i₂ i₃ j h)
      h_1
-- Mathlib.Tactic.FailIfNoProgress
/-- Run `tacs : TacticM Unit` on `goal`, and fail if no progress is made.  -/
Mathlib.Tactic.runAndFailIfNoProgress : Lean.MVarId → Lean.Elab.Tactic.TacticM Unit → Lean.Elab.Tactic.TacticM (List Lean.MVarId)
-- Mathlib.Algebra.Ring.Pi
/-- **Alias** of `RingHom.pi`.

---

A family of ring homomorphisms `f a : γ →+* β a` defines a ring homomorphism
`RingHom.pi f : γ →+* Π a, β a` given by `RingHom.pi f x b = f b x`.  -/
Pi.ringHom : {I : Type u} →
  {f : I → Type u_1} →
    {γ : Type u_2} →
      [inst : (i : I) → NonAssocSemiring (f i)] →
        [inst_1 : NonAssocSemiring γ] → ((i : I) → γ →+* f i) → γ →+* (i : I) → f i
-- Mathlib.Data.Quot
Quotient.eval_mk : ∀ {ι : Type u_3} {α : ι → Type u_4} {S : (i : ι) → Setoid (α i)} (f : (i : ι) → α i), ⟦f⟧.eval = fun i => ⟦f i⟧
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Example.val.sizeOf_spec : ∀ (a : Lean.Expr), sizeOf (Lean.Meta.Match.Example.val a) = 1 + sizeOf a
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.mk.injEq : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (toFun : R → ℝ) (mono' : Monotone toFun)
  (right_continuous' : ∀ (x : R), ContinuousWithinAt toFun (Set.Ici x) x) (toFun_1 : R → ℝ) (mono'_1 : Monotone toFun_1)
  (right_continuous'_1 : ∀ (x : R), ContinuousWithinAt toFun_1 (Set.Ici x) x),
  ({ toFun := toFun, mono' := mono', right_continuous' := right_continuous' } =
      { toFun := toFun_1, mono' := mono'_1, right_continuous' := right_continuous'_1 }) =
    (toFun = toFun_1)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.le_maxD_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  t.contains k = true → ∀ {fallback : α}, (cmp k (t.maxD fallback)).isLE = true
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.instZero.eq_1 : ∀ {α : Type u} [inst : AddMonoid α], AddUnits.instZero = { zero := { val := 0, neg := 0, val_neg := ⋯, neg_val := ⋯ } }
-- Mathlib.RingTheory.NormalClosure
Ring.instNontrivialNormalClosure : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : IsDomain S]
  [inst_4 : Algebra R S] [inst_5 : Module.IsTorsionFree R S], Nontrivial (Ring.NormalClosure R S)
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
Std.Iter.toArray_flatMapM : ∀ {α α₂ β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α Id β] [inst_5 : Std.Iterator α₂ m γ] [Std.Iterators.Finite α Id]
  [Std.Iterators.Finite α₂ m] {f : β → m (Std.IterM m γ)} {it₁ : Std.Iter β},
  (Std.Iter.flatMapM f it₁).toArray =
    Array.flatten <$>
      (Std.Iter.mapM
          (fun b => do
            let __do_lift ← f b
            __do_lift.toArray)
          it₁).toArray
-- Mathlib.Algebra.Free
FreeAddSemigroup.lift_comp_of : ∀ {α : Type u} {β : Type v} [inst : AddSemigroup β] (f : α → β), ⇑(FreeAddSemigroup.lift f) ∘ FreeAddSemigroup.of = f
-- Mathlib.Topology.Algebra.Support
mulTSupport.eq_1 : ∀ {X : Type u_1} {α : Type u_2} [inst : One α] [inst_1 : TopologicalSpace X] (f : X → α),
  mulTSupport f = closure (Function.mulSupport f)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.IsInvertible.inverse_comp_of_right : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} [inst : TopologicalSpace M]
  [inst_1 : TopologicalSpace M₂] [inst_2 : TopologicalSpace M₃] [inst_3 : Semiring R] [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R M₂] [inst_8 : AddCommMonoid M₃]
  [inst_9 : Module R M₃] {g : M₂ →L[R] M₃} {f : M →L[R] M₂},
  f.IsInvertible → (g ∘SL f).inverse = f.inverse ∘SL g.inverse
-- Mathlib.CategoryTheory.ConcreteCategory.Bundled
CategoryTheory.Bundled.mk.sizeOf_spec : ∀ {c : Type u → Type v} [inst : (a : Type u) → SizeOf (c a)] (α : Type u)
  (str : autoParam (c α) CategoryTheory.Bundled.str._autoParam),
  sizeOf { α := α, str := str } = 1 + sizeOf α + sizeOf str
-- Init.Data.UInt.Lemmas
UInt16.ofNatLT_lt_iff_lt : ∀ {a b : ℕ} (ha : a < UInt16.size) (hb : b < UInt16.size), UInt16.ofNatLT a ha < UInt16.ofNatLT b hb ↔ a < b
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.instMonoM : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : P.IsProper] (j : ι), CategoryTheory.Mono (f.m j)
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.toSubalgebra_subtype : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] (S : StarSubalgebra R A), S.val = ↑S.subtype
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_eq_on_Ioc : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] (z : ℤ),
  ∀ a ∈ Set.Ioc (↑z - 1) ↑z, ⌈a⌉ = z
-- Init.Data.Nat.Lemmas
Nat.le_self_pow : ∀ {n : ℕ}, n ≠ 0 → ∀ (a : ℕ), a ≤ a ^ n
-- Mathlib.NumberTheory.ModularForms.Basic
instFactIsCuspInftyRealOfIsArithmetic : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic], Fact (IsCusp OnePoint.infty Γ)
-- Mathlib.Order.Atoms
IsAtomistic.instIsAtomic : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α] [IsAtomistic α], IsAtomic α
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Compacts.isUniformEmbedding_coe : ∀ {α : Type u_1} [inst : UniformSpace α], IsUniformEmbedding SetLike.coe
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- A functor `F` preserves biproducts if it preserves biproducts of any shape `J` of size `w`.
The usual notion of preservation of biproducts is recovered by choosing `w` to be the universe
of the morphisms of `C`.  -/
CategoryTheory.Limits.PreservesBiproducts : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (F : CategoryTheory.Functor C D) → [F.PreservesZeroMorphisms] → Prop
-- Mathlib.SetTheory.Ordinal.Notation
ONote.le_def : ∀ {x y : ONote}, x ≤ y ↔ x.repr ≤ y.repr
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.LambdaTheoremType.comp.sizeOf_spec : sizeOf Mathlib.Meta.FunProp.LambdaTheoremType.comp = 1
-- Mathlib.Data.List.Defs
/-- `permutations'Aux t ts` inserts `t` into every position in `ts`, including the last.
This function is intended for use in specifications, so it is simpler than `permutationsAux2`,
which plays roughly the same role in `permutations`.

Note that `(permutationsAux2 t [] [] ts id).2` is similar to this function, but skips the last
position:

```
    permutations'Aux 10 [1, 2, 3] =
      [[10, 1, 2, 3], [1, 10, 2, 3], [1, 2, 10, 3], [1, 2, 3, 10]]
    (permutationsAux2 10 [] [] [1, 2, 3] id).2 =
      [[10, 1, 2, 3], [1, 10, 2, 3], [1, 2, 10, 3]]
```
 -/
List.permutations'Aux : {α : Type u_1} → α → List α → List (List α)
-- Mathlib.Topology.MetricSpace.PiNat
/-- If the functions `f i : X → Y i` separate points of `X`, then `X` can be embedded into
`∀ i, Y i`.  -/
Metric.PiNatEmbed.emetricSpace : {ι : Type u_2} →
  {X : Type u_3} →
    {Y : ι → Type u_4} →
      {f : (i : ι) → X → Y i} →
        [Encodable ι] →
          [(i : ι) → EMetricSpace (Y i)] →
            (Pairwise fun x y => ∃ i, f i x ≠ f i y) → EMetricSpace (Metric.PiNatEmbed X Y f)
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.SplittingFieldAux.algebraMap_succ : ∀ {K : Type v} [inst : Field K] (n : ℕ) (f : Polynomial K),
  algebraMap K (Polynomial.SplittingFieldAux (n + 1) f) =
    (algebraMap (AdjoinRoot f.factor) (Polynomial.SplittingFieldAux n f.removeFactor)).comp (AdjoinRoot.of f.factor)
-- Std.Do.PredTrans
Std.Do.PredTrans.mk : {ps : Std.Do.PostShape} →
  {α : Type u} →
    (trans : Std.Do.PostCond α ps → Std.Do.Assertion ps) → Std.Do.PredTrans.Conjunctive trans → Std.Do.PredTrans ps α
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMultispan.Hom.snd : {J : CategoryTheory.Limits.MultispanShape} →
  (a : J.L) →
    (CategoryTheory.Limits.WalkingMultispan.left a).Hom (CategoryTheory.Limits.WalkingMultispan.right (J.snd a))
-- Mathlib.Algebra.Group.End
Equiv.mulLeft_mul : ∀ {α : Type u_4} [inst : Group α] (a b : α), Equiv.mulLeft (a * b) = Equiv.mulLeft a * Equiv.mulLeft b
-- Plausible.Testable
/-- A `dbgTrace` with special formatting  -/
Plausible.Testable.slimTrace : {m : Type → Type u_1} → [Pure m] → String → m PUnit.{1}
-- Mathlib.Order.Hom.BoundedLattice
/-- The type of finitary supremum-preserving homomorphisms from `α` to `β`.  -/
SupBotHom : (α : Type u_6) → (β : Type u_7) → [Max α] → [Max β] → [Bot α] → [Bot β] → Type (max u_6 u_7)
-- Mathlib.Analysis.CStarAlgebra.Matrix
Matrix.l2_opNNNorm_conjTranspose_mul_self : ∀ {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} [inst : RCLike 𝕜] [inst_1 : Fintype m] [inst_2 : Fintype n]
  [inst_3 : DecidableEq n] (A : Matrix m n 𝕜), ‖A.conjTranspose * A‖₊ = ‖A‖₊ * ‖A‖₊
-- Mathlib.Analysis.Normed.Group.Defs
/-- Addition is commutative in a commutative additive magma.  -/
ESeminormedAddCommMonoid.add_comm : ∀ {E : Type u_8} {inst : TopologicalSpace E} [self : ESeminormedAddCommMonoid E] (a b : E), a + b = b + a