mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w} [Std.TransCmp cmp]
  {f : (a : α) → β a → γ a} {k fallback : α}, (Std.DTreeMap.map f t).getKeyD k fallback = t.getKeyD k fallback
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addProjection_respects_measure' : ∀ {G : Type u_1} {α : Type u_3} {inst : AddGroup G} {inst_1 : AddAction G α} {inst_2 : MeasurableSpace α}
  {ν : autoParam (MeasureTheory.Measure α) MeasureTheory.AddQuotientMeasureEqMeasurePreimage._auto_1}
  {μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α))}
  [self : MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ] (t : Set α),
  MeasureTheory.IsAddFundamentalDomain G t ν →
    μ = MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (ν.restrict t)
-- Mathlib.LinearAlgebra.AffineSpace.Basis
/-- Given an affine basis for an affine space `P`, if we single out one member of the family, we
obtain a linear basis for the model space `V`.

The linear basis corresponding to the singled-out member `i : ι` is indexed by `{j : ι // j ≠ i}`
and its `j`th element is `b j -ᵥ b i`. (See `basisOf_apply`.)  -/
AffineBasis.basisOf : {ι : Type u_1} →
  {k : Type u_5} →
    {V : Type u_6} →
      {P : Type u_7} →
        [inst : AddCommGroup V] →
          [inst_1 : AddTorsor V P] →
            [inst_2 : Ring k] → [inst_3 : Module k V] → AffineBasis ι k P → (i : ι) → Module.Basis { j // j ≠ i } k V
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
/-- If `∑ i, f i • v i = ∑ i, g i • v i`, then for all `i`, `f i = g i`.  -/
LinearIndependent.eq_coords_of_eq : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Fintype ι] {v : ι → M},
  LinearIndependent R v → ∀ {f g : ι → R}, ∑ i, f i • v i = ∑ i, g i • v i → ∀ (i : ι), f i = g i
-- Mathlib.Algebra.Category.Ring.Under.Basic
AlgHom.toUnder_right : ∀ {R : CommRingCat} {A B : Type u} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra (↑R) A]
  [inst_3 : Algebra (↑R) B] (f : A →ₐ[↑R] B) (a : A),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Under.Hom.right f.toUnder)) a = f a
-- Mathlib.Algebra.Module.Equiv.Basic
DistribMulAction.toLinearEquiv_symm_apply : ∀ (R : Type u_1) {S : Type u_4} (M : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Group S] [inst_4 : DistribMulAction S M] [inst_5 : SMulCommClass S R M] (s : S) (a : M),
  (DistribMulAction.toLinearEquiv R M s).symm a = s⁻¹ • a
-- Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
AlgebraicGeometry.instIsSchemeTheoreticallyDominantOfIsIsoScheme : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [CategoryTheory.IsIso f],
  AlgebraicGeometry.IsSchemeTheoreticallyDominant f
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanced_balanceL : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} (hlb : l.Balanced)
  (hrb : r.Balanced) (hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size r.size),
  (Std.DTreeMap.Internal.Impl.balanceL k v l r hlb hrb hlr).Balanced
-- Mathlib.Topology.MetricSpace.Basic
EMetricSpace.replaceEDist_eq : ∀ {X : Type u_2} (m : EMetricSpace X) (d : X → X → ENNReal) (hd : d = edist), m.replaceEDist d hd = m
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.SimpleFunc.toLargerSpace.congr_simp : ∀ {β : Type u_6} {γ : Type u_7} {m m0 : MeasurableSpace β} (hm : m ≤ m0) (f f_1 : MeasureTheory.SimpleFunc β γ),
  f = f_1 → MeasureTheory.SimpleFunc.toLargerSpace hm f = MeasureTheory.SimpleFunc.toLargerSpace hm f_1
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Filter.iInf_isMeasurablyGenerated : ∀ {α : Type u_1} {ι : Sort uι} [inst : MeasurableSpace α] {f : ι → Filter α} [∀ (i : ι), (f i).IsMeasurablyGenerated],
  (⨅ i, f i).IsMeasurablyGenerated
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.neg_nsmul : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddGroup α],
  Function.Periodic f c → ∀ (n : ℕ), Function.Periodic f (-(n • c))
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.getEntryGE?_eq_find? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {t : Std.DTreeMap.Internal.Impl α β},
  t.Ordered →
    ∀ {k : α}, Std.DTreeMap.Internal.Impl.getEntryGE? k t = List.find? (fun e => (compare e.fst k).isGE) t.toListModel
-- Lean.Meta.CongrTheorems
_private.Lean.Meta.CongrTheorems.0.Lean.Meta.EqInfo.hyp.inj : ∀ {fvarId fvarId_1 : Lean.FVarId}, Lean.Meta.EqInfo.hyp✝ fvarId = Lean.Meta.EqInfo.hyp✝ fvarId_1 → fvarId = fvarId_1
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.antitone : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  (F : I.Filtration M), Antitone F.N
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.dropWhile_string_eq_dropWhile_toSlice : ∀ {pat : String} {s : String.Slice}, s.dropWhile pat = s.dropWhile pat.toSlice
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.unitIso_hom_app_comp_inverse_map_η_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal],
  CategoryTheory.CategoryStruct.comp (e.unitIso.hom.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (e.inverse.map (CategoryTheory.Functor.OplaxMonoidal.η e.functor)) =
    CategoryTheory.Functor.LaxMonoidal.ε e.inverse
-- Mathlib.Algebra.Order.Monoid.NatCast
zero_le_two : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : Preorder α] [ZeroLEOneClass α] [AddLeftMono α], 0 ≤ 2
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.toList_succ_succ_eq_map : ∀ {α : Type u} [inst : LE α] [DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LinearlyUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst : Std.PRange.InfinitelyUpwardEnumerable α] [inst_4 : Std.Rxi.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {lo : α},
  (Std.PRange.succ lo)...*.toList = List.map Std.PRange.succ lo...*.toList
-- Mathlib.Analysis.Calculus.Deriv.Mul
hasDerivAt_const_mul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} (c : 𝕜), HasDerivAt (fun y => c * y) c x
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.eq_of_pairwise_lt_of_mem_iff_mem : ∀ {α : Type u} {lt : α → α → Prop} [asymm : Std.Asymm lt] {l l' : List α},
  List.Pairwise lt l → List.Pairwise lt l' → (∀ (a : α), a ∈ l ↔ a ∈ l') → l = l'
-- Lean.Compiler.Options
Lean.Compiler.compiler.relaxedMetaCheck : Lean.Option Bool
-- Aesop.Forward.State.ApplyGoalDiff
_private.Aesop.Forward.State.ApplyGoalDiff.0.Aesop.ForwardState.applyGoalDiff.updateTarget : Aesop.LocalRuleSet → Aesop.GoalDiff → Aesop.ForwardState → Aesop.BaseM Aesop.ForwardState
-- Init.Data.Int.Bitwise.Basic
/-- Bitwise right shift, usually accessed via the `>>>` operator.

Interprets the integer as an infinite sequence of bits in two's complement and shifts the value to
the right.

Examples:
* `( 0b0111 : Int) >>> 1 =  0b0011`
* `( 0b1000 : Int) >>> 1 =  0b0100`
* `(-0b1000 : Int) >>> 1 = -0b0100`
* `(-0b0111 : Int) >>> 1 = -0b0100`
 -/
Int.shiftRight : ℤ → ℕ → ℤ
-- Init.Data.Fin.Basic
_private.Init.Data.Fin.Basic.0.Fin.modn.match_1.eq_1 : ∀ {n : ℕ} (motive : Fin n → ℕ → Sort u_1) (a : ℕ) (h : a < n) (m : ℕ)
  (h_1 : (a : ℕ) → (h : a < n) → (m : ℕ) → motive ⟨a, h⟩ m),
  (match ⟨a, h⟩, m with
    | ⟨a, h⟩, m => h_1 a h m) =
    h_1 a h m
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- The isomorphism between `(G.mapComposableArrows 2).obj (.mk₂ f g)` and
`.mk₂ (G.map f) (G.map g)`.  -/
CategoryTheory.Functor.mapComposableArrowsObjMk₂Iso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (G : CategoryTheory.Functor C D) →
          {X Y Z : C} →
            (f : X ⟶ Y) →
              (g : Y ⟶ Z) →
                (G.mapComposableArrows 2).obj (CategoryTheory.ComposableArrows.mk₂ f g) ≅
                  CategoryTheory.ComposableArrows.mk₂ (G.map f) (G.map g)
-- Lean.Data.Lsp.Internal
Lean.Lsp.instToJsonLeanQueryModuleParams : Lean.ToJson Lean.Lsp.LeanQueryModuleParams
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.toMeasure_apply_eq_toOuterMeasure_apply : ∀ {α : Type u_1} [inst : MeasurableSpace α] (p : PMF α) {s : Set α},
  MeasurableSet s → p.toMeasure s = p.toOuterMeasure s
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Supermartingale.smul_nonneg : ∀ {Ω : Type u_1} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {ℱ : MeasureTheory.Filtration ι m0} {F : Type u_4} [inst_1 : NormedAddCommGroup F] [inst_2 : PartialOrder F]
  [inst_3 : NormedSpace ℝ F] [CompleteSpace F] [IsOrderedModule ℝ F] {f : ι → Ω → F} {c : ℝ},
  0 ≤ c → MeasureTheory.Supermartingale f ℱ μ → MeasureTheory.Supermartingale (c • f) ℱ μ
-- Mathlib.Order.Cover
WCovBy.le_of_lt : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, a ⩿ b → c < b → c ≤ a
-- Mathlib.Algebra.Group.Equiv.Opposite
AddHom.op.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : Add M] [inst_1 : Add N],
  AddHom.op =
    { toFun := fun f => { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, map_add' := ⋯ },
      invFun := fun f => { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, map_add' := ⋯ }, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.Logic.Basic
/-- On a goal of the form of `x = y`, also try to simplify `y = x`.

If simplifying `y = x` gives `y' = x'` then this simproc returns `x' = y'` (so that the use of
commutativity is transparent), otherwise it returns the result of simplifying `y = x` unmodified.
 -/
eqComm : Lean.Meta.Simp.Simproc
-- Mathlib.CategoryTheory.Comma.Basic
/-- The equality between `map α β ⋙ fst L' R'` and `fst L R ⋙ F₁`,
where `α : F₁ ⋙ L' ⟶ L ⋙ F`.  -/
CategoryTheory.Comma.map_fst : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'}
  {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'}
  (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R'),
  (CategoryTheory.Comma.map α β).comp (CategoryTheory.Comma.fst L' R') = (CategoryTheory.Comma.fst L R).comp F₁
-- Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
/-- The naturality for the left unitor.  -/
Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality.mkNaturalityLeftUnitor : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality m] →
    Mathlib.Tactic.BicategoryLike.NormalizedHom →
      Mathlib.Tactic.BicategoryLike.NormalizedHom →
        Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Lean.Expr
-- Init.Data.Int.DivMod.Lemmas
Int.eq_zero_of_tdiv_eq_zero : ∀ {d n : ℤ}, d ∣ n → n.tdiv d = 0 → n = 0
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.coxeterWeightIn.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [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) (S : Type u_7)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [inst_7 : P.IsValuedIn S] (i j : ι),
  P.coxeterWeightIn S i j = P.pairingIn S i j * P.pairingIn S j i
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
/-- An ordering `O` on a ring `R` is a preordering such that
1. `O` contains either `x` or `-x` for each `x` in `R` and
2. the support of `O` is a prime ideal.
 -/
RingPreordering.IsOrdering : {R : Type u_1} → [inst : CommRing R] → RingPreordering R → Prop
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.triangleIso : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B)
  (G : CategoryTheory.Functor B C),
  F.associator (CategoryTheory.Functor.id B) G ≪≫ F.isoWhiskerLeft G.leftUnitor =
    CategoryTheory.Functor.isoWhiskerRight F.rightUnitor G
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegularWRT.trans : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p q q' : Set α → Prop},
  μ.InnerRegularWRT p q → μ.InnerRegularWRT q q' → μ.InnerRegularWRT p q'
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.isEqBwdPattern? : Lean.Expr → Option (Lean.Expr × Lean.Expr)
-- Lean.Syntax
/-- Advance to the `idx`-th child of the current node.  -/
Lean.Syntax.Traverser.down : Lean.Syntax.Traverser → ℕ → Lean.Syntax.Traverser
-- Mathlib.AlgebraicGeometry.PullbackCarrier
/-- Given `t : X ×[S] Y` with projections to `X`, `Y` and `S` denoted by `x`, `y` and `s`
respectively, this is the canonical map `κ(x) ⊗[κ(s)] κ(y) ⟶ κ(t)`.  -/
AlgebraicGeometry.Scheme.Pullback.ofPointTensor : {X Y S : AlgebraicGeometry.Scheme} →
  {f : X ⟶ S} →
    {g : Y ⟶ S} →
      (t : ↥(CategoryTheory.Limits.pullback f g)) →
        (AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint t).tensor ⟶
          (CategoryTheory.Limits.pullback f g).residueField t
-- Mathlib.Algebra.Group.Commute.Units
/-- If the sum of two commuting elements is an additive unit, then the left summand is
an additive unit.  -/
AddUnits.leftOfAdd : {M : Type u_1} → [inst : AddMonoid M] → (u : AddUnits M) → (a b : M) → a + b = ↑u → AddCommute a b → AddUnits M
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.total.map_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂],
  HomologicalComplex₂.total.map (CategoryTheory.CategoryStruct.id K) c₁₂ =
    CategoryTheory.CategoryStruct.id (K.total c₁₂)
-- Mathlib.Algebra.Module.SpanRank
/-- The minimum cardinality of a generating set of a submodule as a natural number. If no finite
generating set exists, the span rank is defined to be `0`.  -/
Submodule.spanFinrank : {R : Type u_1} →
  {M : Type u} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Submodule R M → ℕ
-- Init.Data.String.Slice
String.Slice.SplitIterator.instIteratorLoopIdSubsliceOfMonad : {ρ : Type} →
  {σ : String.Slice → Type} →
    [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
      {pat : ρ} →
        [inst_1 : String.Slice.Pattern.ToForwardSearcher pat σ] →
          {n : Type u_1 → Type u_2} →
            {s : String.Slice} → [Monad n] → Std.IteratorLoop (String.Slice.SplitIterator pat s) Id n
-- Mathlib.Topology.Bornology.Basic
Filter.Tendsto.eventually_ne_cobounded : ∀ {α : Type u_2} {β : Type u_3} [inst : Bornology α] {f : β → α} {l : Filter β},
  Filter.Tendsto f l (Bornology.cobounded α) → ∀ (a : α), ∀ᶠ (x : β) in l, f x ≠ a
-- Mathlib.Topology.Instances.Matrix
summable_matrix_blockDiagonal' : ∀ {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l → Type u_9} {n' : l → Type u_10} [inst : AddCommMonoid R]
  [inst_1 : TopologicalSpace R] {L : SummationFilter X} [inst_2 : DecidableEq l]
  {f : X → (i : l) → Matrix (m' i) (n' i) R}, Summable (fun x => Matrix.blockDiagonal' (f x)) L ↔ Summable f L
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Pythagorean theorem, subtracting vectors, if-and-only-if vector
inner product form.  -/
norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F),
  ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ inner ℝ x y = 0
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.Localization.SmallHom.mkInv_comp_mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  [inst_1 : CategoryTheory.Localization.HasSmallLocalizedHom W X X]
  [inst_2 : CategoryTheory.Localization.HasSmallLocalizedHom W X Y]
  [inst_3 : CategoryTheory.Localization.HasSmallLocalizedHom W Y X] (f : Y ⟶ X) (hf : W f),
  (CategoryTheory.Localization.SmallHom.mkInv f hf).comp (CategoryTheory.Localization.SmallHom.mk W f) =
    CategoryTheory.Localization.SmallHom.mk W (CategoryTheory.CategoryStruct.id X)
-- Mathlib.Control.Lawful
StateT.run_mapConst : ∀ {σ : Type u} {m : Type u → Type v} {α β : Type u} [inst : Monad m] [LawfulMonad m] (x : StateT σ m α) (y : β)
  (st : σ), (Functor.mapConst y x).run st = Prod.map (Function.const α y) id <$> x.run st
-- Lean.Expr
Lean.Expr.fvarId? : Lean.Expr → Option Lean.FVarId
-- Mathlib.Probability.Kernel.Composition.MeasureComp
MeasureTheory.Measure.instIsZeroOrProbabilityMeasureBindCoeKernelOfIsZeroOrMarkovKernel : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.IsZeroOrProbabilityMeasure μ]
  [ProbabilityTheory.IsZeroOrMarkovKernel κ], MeasureTheory.IsZeroOrProbabilityMeasure (μ.bind ⇑κ)
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.re_neg : ∀ {R : Type u_1} {a b : R} [inst : Neg R] (z : QuadraticAlgebra R a b), (-z).re = -z.re
-- Mathlib.Topology.Order.IsLUB
IsGLB.isLUB_of_tendsto : ∀ {α : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α]
  [inst_3 : Preorder γ] [inst_4 : TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α} {b : γ},
  AntitoneOn f s → IsGLB s a → s.Nonempty → Filter.Tendsto f (nhdsWithin a s) (nhds b) → IsLUB (f '' s) b
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.iSup_eq_bsup : ∀ {o : Ordinal.{u_3}} (f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_3 u_4}), iSup (o.familyOfBFamily f) = o.bsup f
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.isOpen_extend_target : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} [I.Boundaryless], IsOpen (f.extend I).target
-- Mathlib.RingTheory.PowerSeries.Expand
PowerSeries.expand_mul : ∀ {R : Type u_2} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) (q : ℕ) (hq : q ≠ 0) (φ : PowerSeries R),
  (PowerSeries.expand (p * q) ⋯) φ = (PowerSeries.expand p hp) ((PowerSeries.expand q hq) φ)
-- Std.Do.SPred.Notation
/-- Unexpander that reconstructs `spred(... ∨ ...)⌝` syntax from applications of `SPred.or`, lifting
nested applications of `spred(...)` from the arguments.
 -/
Std.Do.SPred.Notation.unexpandOr : Lean.PrettyPrinter.Unexpander
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.closure_eq_preimage_closure_image : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace X],
  Topology.IsInducing f → ∀ (s : Set X), closure s = f ⁻¹' closure (f '' s)
-- Mathlib.Combinatorics.Matroid.Map
Matroid.IsBasis.mapEmbedding : ∀ {α : Type u_1} {β : Type u_2} {I : Set α} {M : Matroid α} {X : Set α},
  M.IsBasis I X → ∀ (f : α ↪ β), (M.mapEmbedding f).IsBasis (⇑f '' I) (⇑f '' X)
-- Lean.Meta.Match.MatcherApp.Basic
Lean.Meta.MatcherApp.toExpr : Lean.Meta.MatcherApp → Lean.Expr
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.BodyState.fixed.injEq : ∀ (remaining remaining_1 : ℕ),
  (Std.Http.Protocol.H1.Reader.BodyState.fixed remaining = Std.Http.Protocol.H1.Reader.BodyState.fixed remaining_1) =
    (remaining = remaining_1)
-- Init.Data.Fin.Lemmas
Fin.instLawfulOrderLT : ∀ {n : ℕ}, Std.LawfulOrderLT (Fin n)
-- Mathlib.Tactic.FunProp.FunctionData
Mathlib.Meta.FunProp.MaybeFunctionData.lam.injEq : ∀ (f f_1 : Lean.Expr),
  (Mathlib.Meta.FunProp.MaybeFunctionData.lam f = Mathlib.Meta.FunProp.MaybeFunctionData.lam f_1) = (f = f_1)
-- Mathlib.Algebra.Polynomial.Homogenize
/-- If `deg p ≤ n`, then `homogenize p n (x, 1) = p x`.  -/
Polynomial.aeval_homogenize_X_one : ∀ {R : Type u_1} [inst : CommSemiring R] (p : Polynomial R) {n : ℕ},
  p.natDegree ≤ n → (MvPolynomial.aeval ![Polynomial.X, 1]) (p.homogenize n) = p
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.BitVec.xor_congr : ∀ (w : ℕ) (lhs rhs lhs' rhs' : BitVec w), lhs' = lhs → rhs' = rhs → lhs' ^^^ rhs' = lhs ^^^ rhs
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
CategoryTheory.categoryFree : (R : Type u_1) →
  [CommRing R] →
    (C : Type u) → [CategoryTheory.Category.{v, u} C] → CategoryTheory.Category.{max u_1 v, u} (CategoryTheory.Free R C)
-- Mathlib.Data.ZMod.Basic
ZMod.natCast_zmod_surjective : ∀ {n : ℕ} [NeZero n], Function.Surjective Nat.cast
-- Mathlib.Analysis.Normed.Operator.NNNorm
ContinuousLinearEquiv.lipschitz : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜₂] [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
  {σ₂₁ : 𝕜₂ →+* 𝕜} [inst_7 : RingHomInvPair σ₁₂ σ₂₁] [inst_8 : RingHomInvPair σ₂₁ σ₁₂] (e : E ≃SL[σ₁₂] F),
  LipschitzWith ‖↑e‖₊ ⇑e
-- Mathlib.Analysis.InnerProductSpace.SingularValues
LinearMap.singularValues_zero : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F]
  [inst_6 : FiniteDimensional 𝕜 F], LinearMap.singularValues 0 = 0
-- Mathlib.Order.Filter.Basic
Filter.GenerateSets.univ : ∀ {α : Type u} {g : Set (Set α)}, Filter.GenerateSets g Set.univ
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
/-- Cast `Hom X Y` as an arrow `X ⟶ Y` of presheaves.  -/
AlgebraicGeometry.PresheafedSpace.Hom.toPshHom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → {X Y : AlgebraicGeometry.PresheafedSpace C} → X.Hom Y → (X ⟶ Y)
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.FirstByte.utf8ByteSize.eq_2 : ByteArray.utf8DecodeChar?.FirstByte.utf8ByteSize✝ ByteArray.utf8DecodeChar?.FirstByte.done = 1
-- Mathlib.Algebra.Notation.Support
Function.range_subset_insert_image_support : ∀ {ι : Type u_1} {M : Type u_3} [inst : Zero M] (f : ι → M), Set.range f ⊆ insert 0 (f '' Function.support f)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.setBlack.eq_2 : ∀ {α : Type u_1} (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α),
  (RBTree.RBNode.node c l v r).setBlack = RBTree.RBNode.node RBTree.RBColor.black l v r
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_sub_div₀ : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [inst : Sub β]
  [MeasurableSub₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ)) →
      ∀ (i j k l : ι), i ≠ k → i ≠ l → j ≠ k → j ≠ l → ProbabilityTheory.Kernel.IndepFun (f i - f j) (f k - f l) κ μ
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.instIsRightCancelAdd : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddZeroClass (β i)] [∀ (i : ι), IsRightCancelAdd (β i)],
  IsRightCancelAdd (Π₀ (i : ι), β i)
-- Mathlib.Analysis.Complex.Order
Complex.monotone_ofReal : Monotone Complex.ofReal