mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_single_mul_mul : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Monoid M] [IsCancelMul M] (x : MonoidAlgebra R M) (r : R)
  (m m' : M), (MonoidAlgebra.single m r * x).coeff (m * m') = r * x.coeff m'
-- Std.Time.DateTime
Std.Time.DateTime.instHAddOffset_1 : HAdd Std.Time.DateTime Std.Time.Week.Offset Std.Time.DateTime
-- Mathlib.MeasureTheory.Group.ModularCharacter
/-- The modular character as a map is `g ↦ μ (· * g⁻¹) / μ`, where `μ` is a left Haar measure.

See also `modularCharacter` that defines the map as a homomorphism.  -/
MeasureTheory.Measure.modularCharacterFun : {G : Type u_1} →
  [inst : TopologicalSpace G] → [inst_1 : Group G] → [IsTopologicalGroup G] → [LocallyCompactSpace G] → G → NNReal
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.FreeGroupoid.liftNatIso_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : Type u₁} [inst_1 : CategoryTheory.Groupoid G]
  (F₁ F₂ : CategoryTheory.Functor (CategoryTheory.FreeGroupoid C) G)
  (τ : (CategoryTheory.FreeGroupoid.of C).comp F₁ ≅ (CategoryTheory.FreeGroupoid.of C).comp F₂) (X : C),
  (CategoryTheory.FreeGroupoid.liftNatIso F₁ F₂ τ).hom.app (CategoryTheory.FreeGroupoid.mk X) = τ.hom.app X
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `antivary_inv_right`. -/
Monovary.inv_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : CommGroup β] [inst_2 : PartialOrder β]
  [IsOrderedMonoid β] {f : ι → α} {g : ι → β}, Monovary f g → Antivary f g⁻¹
-- Mathlib.RingTheory.Valuation.ValuationSubring
Valuation.isNontrivial_valuation_valuationSubring_iff : ∀ {K : Type u} [inst : Field K] {Γ : Type u_1} [inst_1 : LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ),
  v.valuationSubring.valuation.IsNontrivial ↔ v.IsNontrivial
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
/-- Consider a `C^n` map `v : M → E₁` to a vector bundle, over a base map `b₁ : M → B₁`, and
another base map `b₂ : M → B₂`. Given linear maps `ϕ m : E₁ (b₁ m) → E₂ (b₂ m)` depending smoothly
on `m`, one can apply `ϕ m` to `v m`, and the resulting map is `C^n`.

Note that the smoothness of `ϕ` cannot always be stated as smoothness of a map into a manifold,
as the pullback bundles `b₁ *ᵖ E₁` and `b₂ *ᵖ E₂` are smooth manifolds only when `b₁` and `b₂` are
globally smooth, but we want to apply this lemma with only local information. Therefore, we
formulate it using smoothness of `ϕ` read in coordinates.

Version for `ContMDiffAt`. We also give a version for `ContMDiffWithinAt`, but no version for
`ContMDiffOn` or `ContMDiff` as our assumption, written in coordinates, only makes sense around
a point.

For a version with `B₁ = B₂` and `b₁ = b₂`, in which smoothness can be expressed without
`inCoordinates`, see `ContMDiffAt.clm_bundle_apply`.
 -/
ContMDiffAt.clm_apply_of_inCoordinates : ∀ {𝕜 : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {B₁ : Type u_4} {B₂ : Type u_5} {M : Type u_6} {E₁ : B₁ → Type u_7}
  {E₂ : B₂ → Type u_8} [inst : NontriviallyNormedField 𝕜] [inst_1 : (x : B₁) → AddCommGroup (E₁ x)]
  [inst_2 : (x : B₁) → Module 𝕜 (E₁ x)] [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁]
  [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_6 : (x : B₁) → TopologicalSpace (E₁ x)]
  [inst_7 : (x : B₂) → AddCommGroup (E₂ x)] [inst_8 : (x : B₂) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂]
  [inst_10 : NormedSpace 𝕜 F₂] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : (x : B₂) → TopologicalSpace (E₂ x)] {EB₁ : Type u_9} [inst_13 : NormedAddCommGroup EB₁]
  [inst_14 : NormedSpace 𝕜 EB₁] {HB₁ : Type u_10} [inst_15 : TopologicalSpace HB₁] {IB₁ : ModelWithCorners 𝕜 EB₁ HB₁}
  [inst_16 : TopologicalSpace B₁] [inst_17 : ChartedSpace HB₁ B₁] {EB₂ : Type u_11} [inst_18 : NormedAddCommGroup EB₂]
  [inst_19 : NormedSpace 𝕜 EB₂] {HB₂ : Type u_12} [inst_20 : TopologicalSpace HB₂] {IB₂ : ModelWithCorners 𝕜 EB₂ HB₂}
  [inst_21 : TopologicalSpace B₂] [inst_22 : ChartedSpace HB₂ B₂] {EM : Type u_13} [inst_23 : NormedAddCommGroup EM]
  [inst_24 : NormedSpace 𝕜 EM] {HM : Type u_14} [inst_25 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM}
  [inst_26 : TopologicalSpace M] [inst_27 : ChartedSpace HM M] {n : WithTop ℕ∞} [inst_28 : FiberBundle F₁ E₁]
  [inst_29 : VectorBundle 𝕜 F₁ E₁] [inst_30 : FiberBundle F₂ E₂] [inst_31 : VectorBundle 𝕜 F₂ E₂] {b₁ : M → B₁}, ⋯
-- Mathlib.Data.Finset.Erase
Finset.notMem_erase : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), a ∉ s.erase a
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.abs_def : ∀ (q : ℚ), |q| = Rat.divInt ↑q.num.natAbs ↑q.den
-- Mathlib.Data.List.Sort
StrictAnti.sortedGE_listMap : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {l : List α},
  StrictAnti f → ((List.map f l).SortedGE ↔ l.SortedLE)
-- Mathlib.Algebra.Ring.Basic
div_neg_eq_neg_div : ∀ {R : Type u_1} [inst : DivisionMonoid R] [inst_1 : HasDistribNeg R] (a b : R), b / -a = -(b / a)
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffAt.differentiableAt_iteratedFDeriv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : WithTop ℕ∞} {m : ℕ} {x : E}, ContDiffAt 𝕜 n f x → ↑m < n → DifferentiableAt 𝕜 (iteratedFDeriv 𝕜 m f) x
-- Mathlib.FieldTheory.RatFunc.IntermediateField
RatFunc.irreducible_minpolyX' : ∀ {K : Type u_1} [inst : Field K] (f : RatFunc K), (¬∃ c, f = RatFunc.C c) → Irreducible (f.minpolyX ↥K[f])
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instDivInvMonoid : {α : Type u_1} → {l : Filter α} → {G : Type u_6} → [DivInvMonoid G] → DivInvMonoid (l.Germ G)
-- Init.Data.Iterators.Basic
Std.IterM.TerminationMeasures.Finite.rel_trans : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β]
  {it it' it'' : Std.IterM.TerminationMeasures.Finite α m}, it.Rel it' → it'.Rel it'' → it.Rel it''
-- Std.Time.Zoned.Database.Windows
Std.Time.Database.WindowsDb.inst : Std.Time.Database Std.Time.Database.WindowsDb
-- Mathlib.Order.Hom.Bounded
/-- Reinterpret a top homomorphism as a bot homomorphism between the dual lattices.  -/
TopHom.dual : {α : Type u_2} →
  {β : Type u_3} →
    [inst : LE α] → [inst_1 : OrderTop α] → [inst_2 : LE β] → [inst_3 : OrderTop β] → TopHom α β ≃ BotHom αᵒᵈ βᵒᵈ
-- Init.Data.SInt.Lemmas
Int32.toInt_minValue_lt_zero : Int32.minValue.toInt < 0
-- Mathlib.Tactic.Subsingleton
/-- Synthesizes a `Subsingleton ty` instance with the additional local instances made available.  -/
Lean.Meta.synthSubsingletonInst : Lean.Expr → optParam (Array (Lean.Term × Lean.Meta.AbstractMVarsResult)) #[] → Lean.MetaM Lean.Expr
-- Mathlib.Computability.Primrec.Basic
Nat.Primrec.below.zero : ∀ {motive : (a : ℕ → ℕ) → Nat.Primrec a → Prop}, Nat.Primrec.below Nat.Primrec.zero
-- Mathlib.FieldTheory.Galois.Infinite
/-- The Galois correspondence as a `GaloisCoinsertion`  -/
InfiniteGalois.GaloisCoinsertionIntermediateFieldSubgroup : {k : Type u_1} →
  {K : Type u_2} →
    [inst : Field k] →
      [inst_1 : Field K] →
        [inst_2 : Algebra k K] →
          [IsGalois k K] →
            GaloisCoinsertion (⇑OrderDual.toDual ∘ fun E => E.fixingSubgroup)
              ((fun H => IntermediateField.fixedField H) ∘ ⇑OrderDual.toDual)
-- Mathlib.FieldTheory.Separable
Subalgebra.isSeparable_iff : ∀ {F : Type u_1} {L : Type u_2} [inst : CommRing F] [inst_1 : Ring L] [inst_2 : Algebra F L] {S : Subalgebra F L},
  Algebra.IsSeparable F ↥S ↔ ∀ x ∈ S, IsSeparable F x
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
/-- In 2D, the line defined by `s.orthRadius p` intersects `s` at at most two points so long as `p`
lies within `s` and not at its center.

This version provides expressions for those points in terms of an arbitrary vector in
`s.orthRadius p` with norm `1`.  -/
EuclideanGeometry.Sphere.inter_orthRadius_eq_of_dist_le_radius_of_norm_eq_one : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hf2 : Fact (Module.finrank ℝ V = 2)] {s : EuclideanGeometry.Sphere P} {p : P},
  dist p s.center ≤ s.radius →
    p ≠ s.center →
      ∀ {v : V},
        v ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ →
          ‖v‖ = 1 →
            Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) =
              {√(s.radius ^ 2 - dist p s.center ^ 2) • v +ᵥ p, -√(s.radius ^ 2 - dist p s.center ^ 2) • v +ᵥ p}
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.norm_sub_eq_max : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] {R : Type u_4}
  [inst_2 : NonUnitalSeminormedRing R] [IsCancelMulZero R] {f g : C(α, R)}, f * g = 0 → ‖f - g‖ = max ‖f‖ ‖g‖
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.instInhabitedExpr.default : Nat.Internal.Linear.Expr
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_diff_of_contains_eq_false_left : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β] (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α},
      Std.DTreeMap.Internal.Impl.contains k m₁ = false →
        Std.DTreeMap.Internal.Impl.Const.get! (m₁.diff m₂ ⋯) k = default
-- Init.Data.Array.Find
Array.findIdx?_eq_fst_find?_zipIdx : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool},
  Array.findIdx? p xs =
    Option.map (fun x => x.2)
      (Array.find?
        (fun x =>
          match x with
          | (x, snd) => p x)
        xs.zipIdx)
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteElement.val_one : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K], ↑1 = 1
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.builder_nameApply : Lean.ParserDescr
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.sdiff_fundamentalFrontier : ∀ (G : Type u_1) {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (s : Set α),
  s \ MeasureTheory.fundamentalFrontier G s = MeasureTheory.fundamentalInterior G s
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedParam.default : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Param pu
-- Mathlib.Order.Basic
Prod.swap_lt_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {a : α} {b : β} {x : α × β},
  x.swap < (b, a) ↔ x < (a, b)
-- Mathlib.Probability.Distributions.Gaussian.Basic
ProbabilityTheory.IsGaussian.mk : ∀ {E : Type u_1} [inst : TopologicalSpace E] [inst_1 : AddCommMonoid E] [inst_2 : Module ℝ E] {mE : MeasurableSpace E}
  {μ : MeasureTheory.Measure E},
  (∀ (L : StrongDual ℝ E),
      MeasureTheory.Measure.map (⇑L) μ =
        ProbabilityTheory.gaussianReal (∫ (x : E), L x ∂μ) (ProbabilityTheory.variance (⇑L) μ).toNNReal) →
    ProbabilityTheory.IsGaussian μ
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.map_map : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  {δ : α → Type w'} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : (a : α) → β a → γ a} {g : (a : α) → γ a → δ a},
  Std.ExtDHashMap.map g (Std.ExtDHashMap.map f m) = Std.ExtDHashMap.map (fun k v => g k (f k v)) m
-- Mathlib.Algebra.Order.Ring.Abs
abs_pow : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsOrderedRing α] (a : α) (n : ℕ), |a ^ n| = |a| ^ n
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- **Ruzsa's triangle inequality**. Invmul-invmul-invmul version.  -/
Finset.ruzsa_triangle_inequality_invMul_invMul_invMul : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : Group G] (A B C : Finset G),
  B.card * (A⁻¹ * C).card ≤ (B⁻¹ * A).card * (B⁻¹ * C).card
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.restrictScalars_le_iff : ∀ (K : Type u_1) {L : Type u_2} {E : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field E]
  [inst_3 : Algebra K L] [inst_4 : Algebra K E] [inst_5 : Algebra L E] [inst_6 : IsScalarTower K L E]
  {E₁ E₂ : IntermediateField L E},
  IntermediateField.restrictScalars K E₁ ≤ IntermediateField.restrictScalars K E₂ ↔ E₁ ≤ E₂
-- Mathlib.GroupTheory.GroupAction.Hom
VAddCommClass.toAddActionHom_apply : ∀ {M : Type u_11} (N : Type u_9) (α : Type u_10) [inst : VAdd M α] [inst_1 : VAdd N α] [inst_2 : VAddCommClass M N α]
  (c : M) (x : α), (VAddCommClass.toAddActionHom N α c) x = c +ᵥ x
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.restr_eqOnSource_restr : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {s s' : Set X},
  e.source ∩ interior s = e.source ∩ interior s' → e.restr s ≈ e.restr s'
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.isMonicOfDegree_add_add_two : ∀ {R : Type u_1} [inst : Semiring R] [Nontrivial R] (a b : R),
  (Polynomial.X ^ 2 + Polynomial.C a * Polynomial.X + Polynomial.C b).IsMonicOfDegree 2
-- Init.Data.Rat.Lemmas
Rat.add_def : ∀ (a b : ℚ), a + b = Rat.normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den) ⋯
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.mk'' : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Monoid G] →
          [inst_1 : Ring R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : TopologicalSpace V] →
                [inst_4 : IsTopologicalAddGroup V] →
                  [inst_5 : Module R V] →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : TopologicalSpace W] →
                        [inst_8 : IsTopologicalAddGroup W] →
                          [inst_9 : Module R W] →
                            {π₁ : ContRepresentation R G V} →
                              {π₂ : ContRepresentation R G W} →
                                (toContinuousLinearEquiv : V ≃L[R] W) →
                                  (cont :
                                      autoParam (Continuous (↑↑toContinuousLinearEquiv).toFun)
                                        ContinuousLinearMap.cont._autoParam) →
                                    (∀ (g : G),
                                        { toLinearMap := ↑↑toContinuousLinearEquiv, cont := cont } ∘SL π₁ g =
                                          π₂ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv, cont := cont }) →
                                      π₁.Equiv π₂
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.nontrivial_iff_ne_bot : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {N : LieSubmodule R L M}, Nontrivial ↥N ↔ N ≠ ⊥
-- Mathlib.NumberTheory.Padics.WithVal
/-- The `p`-adic integers are isomorphic as uniform spaces to the integers of the uniform completion
of the rationals at the `p`-adic valuation.  -/
PadicInt.withValIntegersUniformEquiv : {p : ℕ} → [inst : Fact (Nat.Prime p)] → ↥(Valued.integer (Rat.padicValuation p).Completion) ≃ᵤ ℤ_[p]
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.sumEquivOfFintype_apply : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7)
  [inst_1 : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : Fintype ι]
  [inst_4 : DecidableEq ι] (x : DirectSum ι fun j => AdicCompletion I (M j)),
  (AdicCompletion.sumEquivOfFintype I M) x = (AdicCompletion.sum I M) x
-- Init.Data.SInt.Lemmas
ISize.toInt32_mul : ∀ (a b : ISize), (a * b).toInt32 = a.toInt32 * b.toInt32
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.veq_mul_right_comm : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] (x y z : R), x * y * z =ᵥ x * z * y
-- Lean.Elab.Tactic.RCases
/-- Expand a list of `rintroPat` into an equivalent list of `rcasesPat` patterns.  -/
Lean.Elab.Tactic.RCases.expandRIntroPats : Array (Lean.TSyntax `rintroPat) →
  optParam (Array (Lean.TSyntax `rcasesPat)) #[] → optParam (Option Lean.Term) none → Array (Lean.TSyntax `rcasesPat)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_le_size_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : Option (β k) → Option (β k)}, m.size - 1 ≤ (m.alter k f).size
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.prod_nsmul : ∀ {M : Type u_5} [inst : CommMonoid M] (m : Multiset M) (n : ℕ), (n • m).prod = m.prod ^ n
-- Mathlib.Data.Num.ZNum
ZNum.bit1.eq_3 : ∀ (a : PosNum), (ZNum.neg a).bit1 = ZNum.neg (Num.casesOn a.pred' 1 PosNum.bit1)
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
_private.Init.Data.String.Lemmas.Pattern.String.ForwardPattern.0.String.Slice.Pos.revSkipWhile.eq_1 : ∀ {ρ : Type} {s : String.Slice} (pos : s.Pos) (pat : ρ) [inst : String.Slice.Pattern.BackwardPattern pat],
  pos.revSkipWhile pat =
    match pos.revSkip? pat with
    | some nextCurr => if nextCurr < pos then nextCurr.revSkipWhile pat else pos
    | none => pos
-- Batteries.Recycling.RBTree.Lemmas
/-- The value `x` returned by `lowerBoundP?` is less or equal to the `cut`.  -/
RBTree.RBSet.lowerBoundP?_le : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {x : α} {t : RBTree.RBSet α cmp},
  t.lowerBoundP? cut = some x → cut x ≠ Ordering.lt
-- Mathlib.Data.Fin.Tuple.Basic
_private.Mathlib.Data.Fin.Tuple.Basic.0.Fin.findX : {n : ℕ} → (p : Fin n → Prop) → [DecidablePred p] → (∃ k, p k) → { i // p i ∧ ∀ j < i, ¬p j }
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpIndL1Fin_add : ∀ {α : Type u_1} {G : Type u_4} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s : Set α} [inst_1 : NormedSpace ℝ G] {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)]
  (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x y : G),
  MeasureTheory.condExpIndL1Fin hm hs hμs (x + y) =
    MeasureTheory.condExpIndL1Fin hm hs hμs x + MeasureTheory.condExpIndL1Fin hm hs hμs y
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
/-- The (limit) cone expressing that the limit of `functorEnrichedHom V F₁ F₂`
is `enrichedHom V F₁ F₂`.  -/
CategoryTheory.Enriched.FunctorCategory.coneFunctorEnrichedHom : (V : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} C] →
          {J : Type u₃} →
            [inst_3 : CategoryTheory.Category.{v₃, u₃} J] →
              [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] →
                (F₁ F₂ : CategoryTheory.Functor J C) →
                  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂] →
                    [CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] →
                      CategoryTheory.Limits.Cone (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₂)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.mk.injEq : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace Z] {proj : Z → B} (toOpenPartialHomeomorph : OpenPartialHomeomorph Z (B × F))
  (baseSet : Set B) (open_baseSet : IsOpen baseSet) (source_eq : toOpenPartialHomeomorph.source = proj ⁻¹' baseSet)
  (target_eq : toOpenPartialHomeomorph.target = baseSet ×ˢ Set.univ)
  (proj_toFun : ∀ p ∈ toOpenPartialHomeomorph.source, (↑toOpenPartialHomeomorph p).1 = proj p)
  (toOpenPartialHomeomorph_1 : OpenPartialHomeomorph Z (B × F)) (baseSet_1 : Set B) (open_baseSet_1 : IsOpen baseSet_1)
  (source_eq_1 : toOpenPartialHomeomorph_1.source = proj ⁻¹' baseSet_1)
  (target_eq_1 : toOpenPartialHomeomorph_1.target = baseSet_1 ×ˢ Set.univ)
  (proj_toFun_1 : ∀ p ∈ toOpenPartialHomeomorph_1.source, (↑toOpenPartialHomeomorph_1 p).1 = proj p),
  ({ toOpenPartialHomeomorph := toOpenPartialHomeomorph, baseSet := baseSet, open_baseSet := open_baseSet,
        source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun } =
      { toOpenPartialHomeomorph := toOpenPartialHomeomorph_1, baseSet := baseSet_1, open_baseSet := open_baseSet_1,
        source_eq := source_eq_1, target_eq := target_eq_1, proj_toFun := proj_toFun_1 }) =
    (toOpenPartialHomeomorph = toOpenPartialHomeomorph_1 ∧ baseSet = baseSet_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- The natural isomorphism between a pushout cocone and the corresponding pushout cocone
reconstructed using `PushoutCocone.mk`.  -/
CategoryTheory.Limits.PushoutCocone.eta : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : X ⟶ Y} →
        {g : X ⟶ Z} →
          (t : CategoryTheory.Limits.PushoutCocone f g) → t ≅ CategoryTheory.Limits.PushoutCocone.mk t.inl t.inr ⋯
-- Mathlib.Algebra.BigOperators.Expect
/-- Reorder an average.

The difference with `Finset.expect_nbij` is that the bijection is specified with an inverse, rather
than as a surjective injection.

The difference with `Finset.expect_bij'` is that the bijection and its inverse are non-dependent
functions, rather than being allowed to use membership of the domains of the averages.

The difference with `Finset.expect_equiv` is that bijectivity is only required to hold on the
domains of the averages, rather than on the entire types.  -/
Finset.expect_nbij' : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] {s : Finset ι}
  {f : ι → M} {t : Finset κ} {g : κ → M} (i : ι → κ) (j : κ → ι),
  (∀ a ∈ s, i a ∈ t) →
    (∀ a ∈ t, j a ∈ s) →
      (∀ a ∈ s, j (i a) = a) →
        (∀ a ∈ t, i (j a) = a) → (∀ a ∈ s, f a = g (i a)) → (s.expect fun i => f i) = t.expect fun i => g i
-- Init.Data.List.Nat.Basic
_private.Init.Data.List.Nat.Basic.0.List.dropLast.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive []) (h_2 : (head : α) → motive [head])
  (h_3 : (a : α) → (as : List α) → motive (a :: as)),
  (match [] with
    | [] => h_1 ()
    | [head] => h_2 head
    | a :: as => h_3 a as) =
    h_1 ()
-- Mathlib.Data.DFinsupp.Small
Finsupp.small : ∀ {σ : Type u_1} {R : Type u_2} [inst : Zero R] [Small.{u, u_2} R] [Small.{u, u_1} σ], Small.{u, max u_2 u_1} (σ →₀ R)
-- Lean.Elab.Quotation
/-- Pattern disagrees with head check, include in "no" branch only  -/
Lean.Elab.Term.Quotation.MatchResult.uncovered : Lean.Elab.Term.Quotation.MatchResult
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.martingale_iff : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0} [CompleteSpace E] [inst_4 : PartialOrder E],
  MeasureTheory.Martingale f ℱ μ ↔ MeasureTheory.Supermartingale f ℱ μ ∧ MeasureTheory.Submartingale f ℱ μ
-- Mathlib.Algebra.Order.Field.Basic
le_of_forall_sub_le : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α},
  (∀ ε > 0, b - ε ≤ a) → b ≤ a
-- Lean.Language.Basic
Lean.Language.SnapshotTree.brecOn_2.eq : ∀ {motive_1 : Lean.Language.SnapshotTree → Sort u}
  {motive_2 : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Sort u}
  {motive_3 : List (Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Sort u}
  {motive_4 : Lean.Language.SnapshotTask Lean.Language.SnapshotTree → Sort u}
  {motive_5 : Task Lean.Language.SnapshotTree → Sort u}
  (t : List (Lean.Language.SnapshotTask Lean.Language.SnapshotTree))
  (F_1 : (t : Lean.Language.SnapshotTree) → t.below → motive_1 t)
  (F_2 :
    (t : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)) →
      Lean.Language.SnapshotTree.below_1 t → motive_2 t)
  (F_3 :
    (t : List (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)) →
      Lean.Language.SnapshotTree.below_2 t → motive_3 t)
  (F_4 :
    (t : Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Lean.Language.SnapshotTree.below_3 t → motive_4 t)
  (F_5 : (t : Task Lean.Language.SnapshotTree) → Lean.Language.SnapshotTree.below_4 t → motive_5 t),
  Lean.Language.SnapshotTree.brecOn_2 t F_1 F_2 F_3 F_4 F_5 =
    F_3 t (Lean.Language.SnapshotTree.brecOn_2.go t F_1 F_2 F_3 F_4 F_5).2