mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.Module
Matrix.Module.scalar_smul : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (r : R) (v : ι → M), (Matrix.scalar ι) r • v = r • v
-- Init.Data.List.Attach
List.attach_map : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β},
  (List.map f l).attach =
    List.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨f x, ⋯⟩)
      l.attach
-- Mathlib.Tactic.IntervalCases
Mathlib.Tactic.IntervalCases.of_not_le_right : ∀ {α : Type u_1} {a b b' : α} [inst : LE α], ¬a ≤ b → b = b' → ¬a ≤ b'
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.rpow_natCast : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] (a : A) (n : ℕ), autoParam (0 ≤ a) CFC.rpow_natCast._auto_1 → a ^ ↑n = a ^ n
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.toIsometryEquiv_trans : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {E : Type u_5} {E₂ : Type u_6} {E₃ : Type u_7} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {σ₁₃ : R →+* R₃} {σ₃₁ : R₃ →+* R}
  {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [inst_3 : RingHomInvPair σ₁₂ σ₂₁] [inst_4 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_5 : RingHomInvPair σ₁₃ σ₃₁] [inst_6 : RingHomInvPair σ₃₁ σ₁₃] [inst_7 : RingHomInvPair σ₂₃ σ₃₂]
  [inst_8 : RingHomInvPair σ₃₂ σ₂₃] [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_10 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
  [inst_11 : SeminormedAddCommGroup E] [inst_12 : SeminormedAddCommGroup E₂] [inst_13 : SeminormedAddCommGroup E₃]
  [inst_14 : Module R E] [inst_15 : Module R₂ E₂] [inst_16 : Module R₃ E₃] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (e' : E₂ ≃ₛₗᵢ[σ₂₃] E₃),
  (e.trans e').toIsometryEquiv = e.toIsometryEquiv.trans e'.toIsometryEquiv
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.monoidal_leftUnitor_inv_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.Comon C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv.hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.X).inv
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (CategoryTheory.CategoryStruct.id
                (Opposite.op
                  (CategoryTheory.Comon.MonOpOpToComonObj
                      (CategoryTheory.MonoidalCategoryStruct.tensorUnit
                        (CategoryTheory.Mon Cᵒᵖ))).ComonToMonOpOpObj)).unop.hom.unop
        X.X)
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.endEquivAutGalois.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F],
  CategoryTheory.PreGaloisCategory.endEquivAutGalois F = CategoryTheory.PreGaloisCategory.endEquivAutGalois F
-- Mathlib.Tactic.FunProp.ToBatteries
/-- Swaps bvars indices `i` and `j`

NOTE: the indices `i` and `j` do not correspond to the `n` in `bvar n`. Rather
they behave like indices in `Expr.lowerLooseBVars`, `Expr.liftLooseBVars`, etc.

TODO: This has to have a better implementation, but I'm still beyond confused with how bvar
indices work
 -/
Lean.Expr.swapBVars : Lean.Expr → ℕ → ℕ → Lean.Expr
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. `lowerBound? k` retrieves the largest entry smaller than or equal to `k`,
if it exists.
 -/
RBTree.RBSet.lowerBound? : {α : Type u_1} → {cmp : α → α → Ordering} → RBTree.RBSet α cmp → α → Option α
-- Lean.Parser.Extra
/-- No-op parser combinator that advises the pretty printer to emit a `Format.group` node.  -/
Lean.Parser.ppRealGroup : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.RepresentationTheory.Coinduced
/-- If `ρ : Representation k G A` and `φ : G →* H` then `coind φ ρ` is the representation
coinduced by `ρ` along `φ`, defined as the following action of `H` on the submodule `coindV φ ρ`
of `G`-equivariant functions from `H` to `A`: we let `h : H` send the function `f : H → A`
to the function sending `h₁` to `f (h₁ * h)`.

See also `Rep.coind` and `Representation.coind'` for variants involving the category `Rep k G`.
 -/
Representation.coind : {k : Type u_1} →
  {G : Type u_2} →
    {H : Type u_3} →
      [inst : Semiring k] →
        [inst_1 : Monoid G] →
          [inst_2 : Monoid H] →
            (φ : G →* H) →
              {B : Type u_5} →
                [inst_3 : AddCommMonoid B] →
                  [inst_4 : Module k B] → (ρ : Representation k G B) → Representation k H ↥(Representation.coindV φ ρ)
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.Monoidal.whiskerLeft_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] {F F' G' : CategoryTheory.Functor C D} {β : F' ⟶ G'} {X : C},
  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft F β).app X =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (β.app X)
-- Init.Prelude
Nat.eq_or_lt_of_le : ∀ {n m : ℕ}, n ≤ m → n = m ∨ n < m
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.LebesgueDecomposition.iSup_le_le : ∀ {α : Type u_2} (f : ℕ → α → ENNReal) (n k : ℕ), k ≤ n → f k ≤ fun x => ⨆ k, ⨆ (_ : k ≤ n), f k x
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
/-- If the infinite place `v` is real, then `v.Completion` is isometric to `ℝ`.  -/
NumberField.InfinitePlace.Completion.isometryEquivRealOfIsReal : {K : Type u_1} → [inst : Field K] → {v : NumberField.InfinitePlace K} → v.IsReal → v.Completion ≃ᵢ ℝ
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- If `s ≅ t` and `IsKan (s.whisker h)`, then `IsKan (t.whisker h)`.  -/
CategoryTheory.Bicategory.LeftExtension.IsKan.whiskerOfCommute : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : a ⟶ b} →
        {g : a ⟶ c} →
          (s t : CategoryTheory.Bicategory.LeftExtension f g) →
            (s ≅ t) → {x : B} → (h : c ⟶ x) → (s.whisker h).IsKan → (t.whisker h).IsKan
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
Subgroup.closure_image_isMulIndecomposable_baseOf : ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_1 : LinearOrder S] [Finite ι]
  [inst_3 : InvolutiveInv ι] [inst_4 : CommGroup S] [IsOrderedMonoid S] (v : ι → G),
  (∀ (i : ι), v i⁻¹ = (v i)⁻¹) →
    ∀ (f : G →* S),
      (∀ (i : ι), f (v i) ≠ 1) → Subgroup.closure (v '' IsMulIndecomposable.baseOf v f) = Subgroup.closure (Set.range v)
-- Mathlib.Combinatorics.Matroid.Map
Matroid.instRankFiniteMapEquiv : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.RankFinite] {f : α ≃ β}, (M.mapEquiv f).RankFinite
-- Aesop.ElabM
Aesop.getGoal : Aesop.ElabM Lean.MVarId
-- Mathlib.NumberTheory.ModularForms.SlashActions
/-- The weight `k` action of `GL (Fin 2) ℝ` on functions `f : ℍ → ℂ`.  -/
ModularForm.instSlashActionIntGeneralLinearGroupFinOfNatNatRealForallUpperHalfPlaneComplex : SlashAction ℤ (GL (Fin 2) ℝ) (UpperHalfPlane → ℂ)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
CliffordAlgebra.changeForm_one : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q Q' : QuadraticForm R M} {B : LinearMap.BilinForm R M} (h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q),
  (CliffordAlgebra.changeForm h) 1 = 1
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- If `G n` tends to `f` a.e. and each `‖G n ·‖ₑ` is `AEMeasurable`, then the lower Lebesgue
integral of `‖f ·‖ₑ` is at most the liminf of the lower Lebesgue integral of `‖G n ·‖ₑ`.  -/
MeasureTheory.lintegral_enorm_le_liminf_of_tendsto : ∀ {G : ℕ → ℝ → ℝ} {f : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ},
  (∀ᵐ (x : ℝ) ∂μ, Filter.Tendsto (fun n => G n x) Filter.atTop (nhds (f x))) →
    (∀ (n : ℕ), AEMeasurable (fun x => ‖G n x‖ₑ) μ) →
      ∫⁻ (x : ℝ), ‖f x‖ₑ ∂μ ≤ Filter.liminf (fun n => ∫⁻ (x : ℝ), ‖G n x‖ₑ ∂μ) Filter.atTop
-- Init.Data.SInt.Lemmas
Int32.toBitVec_neg : ∀ (x : Int32), (-x).toBitVec = -x.toBitVec
-- Mathlib.Algebra.Group.Prod
/-- `Prod.map` as a `MonoidHom`.  -/
MonoidHom.prodMap : {M : Type u_3} →
  {N : Type u_4} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] →
        {M' : Type u_6} →
          {N' : Type u_7} →
            [inst_2 : MulOneClass M'] → [inst_3 : MulOneClass N'] → (M →* M') → (N →* N') → M × N →* M' × N'
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
hasFDerivAt_jacobiTheta₂ : ∀ (z : ℂ) {τ : ℂ}, 0 < τ.im → HasFDerivAt (fun p => jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- Given an adjunction, assigning to an algebra over the left adjoint a coalgebra over its right
adjoint and going back is isomorphic to the identity functor.  -/
CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.unitIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor C C} →
      (adj : F ⊣ G) →
        CategoryTheory.Functor.id (CategoryTheory.Endofunctor.Algebra F) ≅
          (CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf adj).comp
            (CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf adj)
-- Mathlib.Topology.MetricSpace.PiNat
Metric.PiNatEmbed.ext_iff : ∀ {ι : Type u_2} {X : Type u_3} {Y : ι → Type u_4} {f : (i : ι) → X → Y i} {x y : Metric.PiNatEmbed X Y f},
  x = y ↔ x.ofPiNat = y.ofPiNat
-- Mathlib.Algebra.Group.Submonoid.Membership
/-- The exponentiation map is an isomorphism from the additive monoid on natural numbers to powers
when it is injective. The inverse is given by the logarithms.  -/
Submonoid.powLogEquiv : {M : Type u_1} →
  [inst : Monoid M] →
    [DecidableEq M] → {n : M} → (Function.Injective fun m => n ^ m) → Multiplicative ℕ ≃* ↥(Submonoid.powers n)
-- Mathlib.RingTheory.Valuation.Basic
/-- The `Valuation` associated to a `AddValuation`.
 -/
Valuation.ofAddValuation : {R : Type u_3} →
  {Γ₀ : Type u_5} →
    [inst : Ring R] → [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] → AddValuation R (Additive Γ₀)ᵒᵈ ≃ Valuation R Γ₀
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
QuotientAddGroup.equivIocMod.eq_1 : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a : α),
  QuotientAddGroup.equivIocMod hp a =
    { toFun := fun b => ⟨⋯.lift b, ⋯⟩, invFun := fun x => ↑↑x, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.RingTheory.Algebraic.Basic
/-- If `x` is algebraic over `R`, then `x` is algebraic over `S` when `S` is an extension of `R`,
and the map from `R` to `S` is injective.  -/
IsAlgebraic.extendScalars : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [IsScalarTower R S A],
  Function.Injective ⇑(algebraMap R S) → ∀ {x : A}, IsAlgebraic R x → IsAlgebraic S x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_diff_add_size_inter_eq_size_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], (m₁ \ m₂).size + (m₁ ∩ m₂).size = m₁.size
-- Mathlib.RingTheory.Ideal.Colon
Ideal.mem_colon_span_singleton : ∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R} {x r : R}, r ∈ Submodule.colon I ↑(Ideal.span {x}) ↔ r * x ∈ I
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.measurable_restrict_cylinderEvents : ∀ {ι : Type u_2} {X : ι → Type u_3} [m : (i : ι) → MeasurableSpace (X i)] (Δ : Set ι), Measurable Δ.domRestrict
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.ofHom_hom : ∀ {X Y : FinBddDistLat} (f : X ⟶ Y), FinBddDistLat.ofHom (FinBddDistLat.Hom.hom f) = f
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew?_eq_insertIfNewₘ : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (a : α)
  (b : β), (Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew? m a b).2 = m.insertIfNewₘ a b
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasTerminal C],
  CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal.inv = 0
-- Mathlib.Data.Fintype.Card
Fintype.ofEquiv_card : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] (f : α ≃ β), Fintype.card β = Fintype.card α
-- Mathlib.Algebra.Module.Submodule.Lattice
/-- The set `{0}` is the bottom element of the lattice of submodules.  -/
Submodule.instBot : {R : Type u_1} →
  {M : Type u_3} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Bot (Submodule R M)
-- Mathlib.Analysis.Complex.Asymptotics
Complex.isBigO_ofReal_left : ∀ {α : Type u_1} {E : Type u_2} [inst : Norm E] {l : Filter α} {f : α → ℝ} {g : α → E},
  (fun x => ↑(f x)) =O[l] g ↔ f =O[l] g
-- Mathlib.Topology.Semicontinuity.Basic
Continuous.comp_upperSemicontinuousOn : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {γ : Type u_4} [inst_1 : LinearOrder γ]
  [inst_2 : TopologicalSpace γ] [OrderTopology γ] {δ : Type u_5} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ]
  [OrderTopology δ] {g : γ → δ} {f : α → γ},
  Continuous g → UpperSemicontinuousOn f s → Monotone g → UpperSemicontinuousOn (g ∘ f) s
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the reverse direction of `sub_nonpos`. -/
sub_nonpos_of_le : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddRightMono α] {a b : α}, a ≤ b → a - b ≤ 0
-- Mathlib.Topology.ContinuousMap.Defs
ContinuousMapClass.mk : ∀ {F : Type u_1} {X : outParam (Type u_2)} {Y : outParam (Type u_3)} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] [inst_2 : FunLike F X Y], (∀ (f : F), Continuous ⇑f) → ContinuousMapClass F X Y
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
/-- A variant of `iteratedDerivWithin_fun_const_smul` without differentiability assumption when
the scalar multiplication is by division ring elements.  -/
iteratedDerivWithin_fun_const_smul_field : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜} {𝕝 : Type u_4} [inst_3 : DivisionSemiring 𝕝]
  [inst_4 : Module 𝕝 F] [SMulCommClass 𝕜 𝕝 F] [ContinuousConstSMul 𝕝 F] (c : 𝕝) (f : 𝕜 → F),
  iteratedDerivWithin n (fun z => c • f z) s x = c • iteratedDerivWithin n f s x
-- Mathlib.Topology.ContinuousOn
continuousAt_prod_of_discrete_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [DiscreteTopology α] {f : α × β → γ} {x : α × β},
  ContinuousAt f x ↔ ContinuousAt (fun x_1 => f (x.1, x_1)) x.2
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
/-- The leading term in a multivariate polynomial is zero if and only if this polynomial is zero.
 -/
MonomialOrder.leadingTerm_eq_zero_iff : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (p : MvPolynomial σ R),
  m.leadingTerm p = 0 ↔ p = 0
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.meet_bot : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P : l}, Lean.Order.meet P Lean.Order.bot = Lean.Order.bot
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.prod_apply : ∀ {X : Type u_1} {X' : Type u_2} {Y : Type u_3} {Y' : Type u_4} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace X'] [inst_2 : TopologicalSpace Y] [inst_3 : TopologicalSpace Y']
  (eX : OpenPartialHomeomorph X X') (eY : OpenPartialHomeomorph Y Y'), ↑(eX.prod eY) = fun p => (↑eX p.1, ↑eY p.2)
-- Mathlib.Topology.Path
Path.continuous_uncurry_extend_of_continuous_family : ∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : Type u_4} [inst_1 : TopologicalSpace ι] {a b : ι → X}
  (γ : (t : ι) → Path (a t) (b t)), Continuous ↿γ → Continuous ↿fun t => ⇑(γ t).extend
-- Mathlib.GroupTheory.Congruence.Basic
Con.mulAction : {α : Type u_4} →
  {M : Type u_5} →
    [inst : Monoid α] →
      [inst_1 : MulOneClass M] → [inst_2 : MulAction α M] → [IsScalarTower α M M] → (c : Con M) → MulAction α c.Quotient
-- Mathlib.Probability.Martingale.Centering
MeasureTheory.martingale_martingalePart : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : ℕ → Ω → E} {ℱ : MeasureTheory.Filtration ℕ m0} [CompleteSpace E],
  MeasureTheory.StronglyAdapted ℱ f →
    (∀ (n : ℕ), MeasureTheory.Integrable (f n) μ) →
      ∀ [MeasureTheory.SigmaFiniteFiltration μ ℱ], MeasureTheory.Martingale (MeasureTheory.martingalePart f ℱ μ) ℱ μ
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kronecker_natCast : ∀ {α : Type u_3} {l : Type u_9} {m : Type u_10} {n : Type u_11} [inst : NonAssocSemiring α] [inst_1 : DecidableEq n]
  (A : Matrix l m α) (b : ℕ), Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A ↑b = Matrix.blockDiagonal fun x => b • A
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.insertListIfNewₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β),
  m.insertListIfNewₘ [] = m
-- Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
CategoryTheory.PreOneHypercover.IsStronglySeparatedFor.isSeparatedFor_sieve₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : C} {E : CategoryTheory.PreOneHypercover X}
  {F : CategoryTheory.Functor Cᵒᵖ (Type u_3)},
  E.IsStronglySeparatedFor F →
    ∀ ⦃i j : E.I₀⦄ ⦃W : C⦄ (p₁ : W ⟶ E.X i) (p₂ : W ⟶ E.X j),
      CategoryTheory.CategoryStruct.comp p₁ (E.f i) = CategoryTheory.CategoryStruct.comp p₂ (E.f j) →
        CategoryTheory.Presieve.IsSeparatedFor F (E.sieve₁ p₁ p₂).arrows
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.exists_mk' : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (T : Turing.Tape Γ), ∃ L R, T = Turing.Tape.mk' L R
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithLowerSet.ofLowerSet_toLowerSet : ∀ {α : Type u_1} (a : α), Topology.WithLowerSet.ofLowerSet (Topology.WithLowerSet.toLowerSet a) = a
-- Mathlib.NumberTheory.Real.Irrational
Irrational.div_natCast : ∀ {x : ℝ}, Irrational x → ∀ {m : ℕ}, m ≠ 0 → Irrational (x / ↑m)
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- `AddGroupExtension N E G` is a short exact sequence of additive groups `0 → N → E → G → 0`.  -/
AddGroupExtension : (N : Type u_1) →
  (E : Type u_2) → (G : Type u_3) → [AddGroup N] → [AddGroup E] → [AddGroup G] → Type (max (max u_1 u_2) u_3)
-- Init.Data.Float.Float
/-- Bit-for-bit conversion from `UInt64`. Interprets a `UInt64` as a `Float`, ignoring the numeric value
and treating the `UInt64`'s bit pattern as a `Float`.

`Float`s and `UInt64`s have the same endianness on all supported platforms. IEEE 754 very precisely
specifies the bit layout of floats.

This function has a logical model in terms of `Float.Model`.
 -/
Float.ofBits : UInt64 → Float
-- Mathlib.Data.Part
Part.eq_none_iff : ∀ {α : Type u_1} {o : Part α}, o = Part.none ↔ ∀ (a : α), a ∉ o
-- Mathlib.LinearAlgebra.RootSystem.Chain
/-- If `α = P.root i` and `β = P.root j` are linearly independent, this is the index of the root
`β + p • α` where `β - q • α, ..., β - α, β, β + α, ..., β + p • α` is the `α`-chain through `β`.

In the absence of linear independence, it takes a junk value.  -/
RootPairing.chainTopIdx : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [Finite ι] →
          [inst : CommRing R] →
            [CharZero R] →
              [IsDomain R] →
                [inst_3 : AddCommGroup M] →
                  [inst_4 : Module R M] →
                    [inst_5 : AddCommGroup N] →
                      [inst_6 : Module R N] → {P : RootPairing ι R M N} → [P.IsCrystallographic] → ι → ι → ι
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.instInhabitedResult : Inhabited Lean.Meta.LetToHave.Result✝
-- Init.Sym.Lemmas
Lean.Sym.ite_true_congr : ∀ {α : Sort u} (c : Prop) {inst : Decidable c} (a b : α) (c' : Prop), c = c' → ∀ {ht : c'}, (if c then a else b) = a
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- the kernel condition for `i`  -/
CategoryTheory.ShortComplex.LeftHomologyData.wi_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (self : S.LeftHomologyData) {Z : C} (h : S.X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.i (CategoryTheory.CategoryStruct.comp S.g h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Init.Data.Rat.Basic
Rat.zpow : ℚ → ℤ → ℚ
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.merge.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Option α → Sort u_2) (h_1 : Unit → motive none none)
  (h_2 : (x : α) → motive (some x) none) (h_3 : (y : α) → motive none (some y))
  (h_4 : (x y : α) → motive (some x) (some y)),
  (match none, none with
    | none, none => h_1 ()
    | some x, none => h_2 x
    | none, some y => h_3 y
    | some x, some y => h_4 x y) =
    h_1 ()
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.edgeDensity_le_one : ∀ {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [inst : (a : α) → DecidablePred (r a)] (s : Finset α) (t : Finset β),
  Rel.edgeDensity r s t ≤ 1
-- Init.Data.String.Basic
String.Slice.Pos.get_eq_utf8DecodeChar : ∀ {s : String.Slice} (pos : s.Pos) (h : pos ≠ s.endPos),
  pos.get h = s.str.toByteArray.utf8DecodeChar (s.startInclusive.offset.byteIdx + pos.offset.byteIdx) ⋯
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.R.congr_simp : ∀ (K : Type u) [inst : CommRing K] (p p_1 : ℕ) (e_p : p = p_1) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p]
  (a a_1 : ℕ × K),
  a = a_1 → ∀ (a_2 a_3 : ℕ × K), a_2 = a_3 → PerfectClosure.R K p a a_2 = PerfectClosure.R K p_1 a_1 a_3
-- Mathlib.Topology.Algebra.NonUnitalStarAlgebra
NonUnitalStarAlgebra.elemental.self_mem : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] [inst_8 : TopologicalSpace A] [inst_9 : IsSemitopologicalSemiring A]
  [inst_10 : ContinuousConstSMul R A] [inst_11 : ContinuousStar A] (x : A), x ∈ NonUnitalStarAlgebra.elemental R x
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.arrow_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (Y : CategoryTheory.Subobject X),
  CategoryTheory.Mono Y.arrow
-- Mathlib.LinearAlgebra.TensorProduct.Tower
LinearEquiv.baseChange_mul : ∀ (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] (e f : M ≃ₗ[R] M),
  LinearEquiv.baseChange R A M M (e * f) = LinearEquiv.baseChange R A M M e * LinearEquiv.baseChange R A M M f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} [inst_1 : Inhabited (β k)],
  (t₁ ∩ t₂).get! k = if k ∈ t₂ then t₁.get! k else default
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_union : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k fallback : α}, (m₁.union m₂).getKeyD k fallback = m₂.getKeyD k (m₁.getKeyD k fallback)
-- Mathlib.Algebra.Star.Subalgebra
Subalgebra.star_mem_star_iff : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] (S : Subalgebra R A) (x : A),
  star x ∈ star S ↔ x ∈ S