mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.flatten.eq_1 : ∀ {α : Type u},
  Stream'.WSeq.flatten =
    Stream'.Seq.corec fun c =>
      match c.destruct with
      | Sum.inl s => Stream'.Seq.omap (fun x => pure x) (Stream'.Seq.destruct s)
      | Sum.inr c' => some (none, c')
-- Mathlib.Geometry.Convex.Cone.Face.Basic
/-- If a cone is a face of two cones simultaneously, then it's also a face of their intersection.  -/
PointedCone.IsFaceOf.inf_right : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {C₁ C₂ F : PointedCone R M},
  F.IsFaceOf C₁ → F.IsFaceOf C₂ → F.IsFaceOf (C₁ ⊓ C₂)
-- Lean.Compiler.ModPkgExt
/-- Returns the standard base of the native symbol for the compiled constant `declName`.

For many constants, this is the full symbol. However, initializers have an additional prefix
\(i.e., `_init_`\) and boxed functions have an additional suffix
\(see `mkMangledBoxedName`\). Furthermore, some constants do not use this stem at all
\(e.g., `main` and definitions with `@[export]`\).
 -/
Lean.getSymbolStem : Lean.Environment → Lean.Name → String
-- Mathlib.Order.Booleanisation
/-- Boolean algebra containing a given generalised Boolean algebra `α` as a sublattice.

This should be thought of as made of a copy of `α` (representing elements of `α`) living under
another copy of `α` (representing complements of elements of `α`).  -/
Booleanisation : Type u_2 → Type u_2
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.edist_toLp_fst : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : SeminormedAddCommGroup α]
  [inst_1 : SeminormedAddCommGroup β] (x₁ x₂ : α), edist (WithLp.toLp p (x₁, 0)) (WithLp.toLp p (x₂, 0)) = edist x₁ x₂
-- Mathlib.Topology.MetricSpace.Infsep
Set.Nontrivial.einfsep_exists_of_finite : ∀ {α : Type u_1} [inst : EDist α] {s : Set α} [Finite ↑s],
  s.Nontrivial → ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.einfsep = edist x y
-- Mathlib.Logic.Basic
exists_prop_of_false : ∀ {p : Prop} {q : p → Prop}, ¬p → ¬∃ (h' : p), q h'
-- Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
/-- We say that a functor `C ⥤ D` into a site is "locally dense" if
for each covering sieve `T` in `D`, `T ∩ mor(C)` generates a covering sieve in `D`.
 -/
CategoryTheory.Functor.LocallyCoverDense : {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] →
        CategoryTheory.Functor C D → CategoryTheory.GrothendieckTopology D → Prop
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_ric_zero_eq_singleton : (*...=0).toList = [0]
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.coe_add : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (f g : CauSeq β abv), ↑(f + g) = ↑f + ↑g
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.opow_dvd_opow_iff : ∀ {a b c : Ordinal.{u_1}}, 1 < a → (a ^ b ∣ a ^ c ↔ b ≤ c)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.getUserConfigOption : {α : Type} → [Lean.KVMap.Value α] → Lean.Option α → Lean.Meta.SimpM α
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.instInhabitedWhiskerLeft : Inhabited Mathlib.Tactic.BicategoryLike.WhiskerLeft
-- Lean.Elab.DocString
/-- Converts a documentation extension's argument into a Lean value.
 -/
Lean.Doc.FromDocArg.fromDocArg : {α : Type} → [self : Lean.Doc.FromDocArg α] → Lean.Doc.DocArg → Lean.Elab.TermElabM α
-- Mathlib.Data.Finset.Lattice.Lemmas
Finset.inter_insert : ∀ {α : Type u_1} [inst : DecidableEq α] {s₁ s₂ : Finset α} {a : α},
  insert a s₁ ∩ s₂ = if a ∈ s₂ then insert a (s₁ ∩ s₂) else s₁ ∩ s₂
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.regular_mod_smul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A : C)
  [inst_2 : CategoryTheory.MonObj A], CategoryTheory.ModObj.smul = CategoryTheory.MonObj.mul
-- Mathlib.Algebra.Lie.Rank
LieModule.exists_isRegular : ∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : Module.Finite R L] [inst_4 : Module.Free R L] [inst_5 : AddCommGroup M] [inst_6 : Module R M]
  [inst_7 : LieRingModule L M] [inst_8 : LieModule R L M] [inst_9 : Module.Finite R M] [inst_10 : Module.Free R M]
  [IsDomain R] [Infinite R], ∃ x, LieModule.IsRegular R M x
-- Mathlib.Data.Rel
SetRel.cod_univ : ∀ {α : Type u_1} {β : Type u_2} [Nonempty α], SetRel.cod Set.univ = Set.univ
-- Init.Data.Range.Polymorphic.PRange
/-- The lower bound of the range. `lower` is included in the range.
   -/
Std.Rco.lower : {α : Type u} → Std.Rco α → α
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_norm_eq_add_idemFst : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddCommGroup α] [inst_1 : SeminormedAddCommGroup β] {p : ENNReal}
  [Fact (1 ≤ p)],
  0 < p.toReal →
    ∀ (x : WithLp p (α × β)), ‖x‖ = (‖WithLp.idemFst x‖ ^ p.toReal + ‖WithLp.idemSnd x‖ ^ p.toReal) ^ (1 / p.toReal)
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.toVal_one : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀),
  WithVal.toVal v 1 = 1
-- Mathlib.Algebra.Polynomial.PartialFractions
/-- Let `R` be a commutative ring and `f : R[X]`. Let `s` be a finite index set.
Let `g i` be a collection of monic and pairwise coprime polynomials indexed by `s`,
and for each `g i` let `n i` be a natural number. Then `f` can be written in the form
`(∏ i ∈ s, g i ^ n i) * (q + ∑ i ∈ s, ∑ j : Fin (n i), r i j / g i ^ (j + 1))`, where
`degree (r i j) < degree (g i)` and the denominator cancels formally.
See `quo_mul_prod_pow_add_sum_rem_mul_prod_pow_unique` for the uniqueness of this representation.  -/
Polynomial.eq_quo_mul_prod_pow_add_sum_rem_mul_prod_pow : ∀ {R : Type u_1} [inst : CommRing R] [Nontrivial R] {ι : Type u_2} [inst_2 : DecidableEq ι] {s : Finset ι}
  (f : Polynomial R) {g : ι → Polynomial R},
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j => IsCoprime (g i) (g j)) →
      ∀ (n : ι → ℕ),
        ∃ q r,
          (∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) ∧
            f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfcHom_nonneg_iff : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [ContinuousSqrt R]
  [StarOrderedRing R] [inst_8 : TopologicalSpace A] [inst_9 : Ring A] [inst_10 : StarRing A] [inst_11 : PartialOrder A]
  [StarOrderedRing A] [inst_13 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A]
  {a : A} (ha : p a) {f : C(↑(spectrum R a), R)}, 0 ≤ (cfcHom ha) f ↔ 0 ≤ f
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.SplitEpi.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        (section_ : Y ⟶ X) →
          autoParam (CategoryTheory.CategoryStruct.comp section_ f = CategoryTheory.CategoryStruct.id Y)
              CategoryTheory.SplitEpi.id._autoParam →
            CategoryTheory.SplitEpi f
-- Lean.Meta.Tactic.Grind.Types
/-- Proof has been flipped.  -/
Lean.Meta.Grind.ENode.flipped : Lean.Meta.Grind.ENode → Bool
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.compProd_apply_univ_le : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ)
  [ProbabilityTheory.IsFiniteKernel η] (a : α), ((κ.compProd η) a) Set.univ ≤ (κ a) Set.univ * η.bound
-- Mathlib.Computability.Partrec
Computable.const : ∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] (s : σ), Computable fun x => s
-- Mathlib.NumberTheory.FactorisationProperties
Nat.not_pseudoperfect_iff_forall : ∀ {n : ℕ}, ¬n.Pseudoperfect ↔ n = 0 ∨ ∀ s ⊆ n.properDivisors, ∑ i ∈ s, i ≠ n
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.exists_finset_of_mem_adjoin : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {S : Set E} {x : E},
  x ∈ IntermediateField.adjoin F S → ∃ T, ↑T ⊆ S ∧ x ∈ IntermediateField.adjoin F ↑T
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.instOneId : {M : Type u_1} →
  [inst : Monoid M] → {A : Type u_4} → [inst_1 : Monoid A] → [inst_2 : MulDistribMulAction M A] → One (A →*[M] A)
-- Mathlib.Analysis.Normed.Module.Ball.Homeomorph
OpenPartialHomeomorph.univUnitBall_source : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E],
  OpenPartialHomeomorph.univUnitBall.source = Set.univ
-- Init.Data.Array.Attach
Array.size_pmap : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {xs : Array α} {H : ∀ a ∈ xs, p a},
  (Array.pmap f xs H).size = xs.size
-- Mathlib.Tactic.FunProp.Core
/-- Try to apply a theorem provided some of the theorem arguments.  -/
Mathlib.Meta.FunProp.tryTheoremWithHint? : Lean.Expr →
  Mathlib.Meta.FunProp.Origin →
    Array (ℕ × Lean.Expr) →
      (Lean.Expr → Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)) →
        optParam Bool false → Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.instPowNat : {G : Type u_1} → [inst : Add G] → {a : G} → Pow (AddConstEquiv G G a a) ℕ
-- Mathlib.Order.OmegaCompletePartialOrder
/-- A family of continuous functions yields a continuous family of functions.  -/
OmegaCompletePartialOrder.ContinuousHom.flip : {β : Type u_3} →
  {γ : Type u_4} →
    [inst : OmegaCompletePartialOrder β] →
      [inst_1 : OmegaCompletePartialOrder γ] → {α : Type u_6} → (α → β →𝒄 γ) → β →𝒄 α → γ
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.reflectionPerm_eq_reflectionPerm_iff_of_isSMulRegular : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i j : ι),
  IsSMulRegular M 2 → (P.reflectionPerm i = P.reflectionPerm j ↔ P.reflection i = P.reflection j)
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instCommGroup : {α : Type u_1} → [CommGroup α] → CommGroup αᵃᵒᵖ
-- Mathlib.Data.Fin.Tuple.Basic
Fin.find_le : ∀ {n : ℕ} {p : Fin n → Prop} [inst : DecidablePred p] {i : Fin n} (hi : p i), Fin.find p ⋯ ≤ i
-- Mathlib.RingTheory.DedekindDomain.LinearDisjoint
_private.Mathlib.RingTheory.DedekindDomain.LinearDisjoint.0.Module.Basis.ofIsCoprimeDifferentIdeal_aux : ∀ (A : Type u_1) (B : Type u_2) {K : Type u_3} {L : Type u_4} [inst : CommRing A] [inst_1 : Field K]
  [inst_2 : Algebra A K] [IsFractionRing A K] [inst_4 : CommRing B] [inst_5 : Field L] [inst_6 : Algebra B L]
  [inst_7 : Algebra A L] [inst_8 : Algebra K L] [FiniteDimensional K L] [inst_10 : IsScalarTower A K L] (R₁ : Type u_5)
  (R₂ : Type u_6) [inst_11 : CommRing R₁] [inst_12 : CommRing R₂] [IsDomain R₁] [inst_14 : Algebra A R₁]
  [inst_15 : Algebra A R₂] [inst_16 : Algebra R₁ B] [inst_17 : Algebra R₂ B] [inst_18 : Algebra R₁ L]
  [inst_19 : Algebra R₂ L] [IsScalarTower A R₁ L] [inst_21 : IsScalarTower R₁ B L] [IsScalarTower R₂ B L]
  [Module.Finite A R₂] {F₁ F₂ : IntermediateField K L} [inst_24 : Algebra R₁ ↥F₁] [inst_25 : Algebra R₂ ↥F₂]
  [Module.IsTorsionFree R₁ ↥F₁] [IsScalarTower A (↥F₂) L] [inst_28 : IsScalarTower A R₂ ↥F₂] [IsScalarTower R₁ (↥F₁) L]
  [IsScalarTower R₂ (↥F₂) L] [Algebra.IsSeparable K ↥F₂] [Algebra.IsSeparable (↥F₁) L] [inst_33 : IsDomain A]
  [inst_34 : IsDedekindDomain B] [inst_35 : IsDedekindDomain R₁] [inst_36 : IsDedekindDomain R₂] [IsFractionRing B L]
  [IsFractionRing R₁ ↥F₁] [IsFractionRing R₂ ↥F₂] [IsIntegrallyClosed A] [IsIntegralClosure B R₁ L]
  [Module.IsTorsionFree R₁ B] [Module.IsTorsionFree R₂ B], ⋯
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey!_alter! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF →
    ∀ {k k' : α} {f : Option β → Option β},
      (Std.DTreeMap.Internal.Impl.Const.alter! k f t).getKey! k' =
        if compare k k' = Ordering.eq then
          if (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true then k else default
        else t.getKey! k'
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- Natural transformations between functors lift to group objects.  -/
CategoryTheory.Functor.mapGrpNatTrans : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            {F F' : CategoryTheory.Functor C D} →
              [inst_4 : F.Monoidal] → [inst_5 : F'.Monoidal] → (F ⟶ F') → (F.mapGrp ⟶ F'.mapGrp)
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
/-- Partial homeomorphisms, defined on open subsets of the space  -/
OpenPartialHomeomorph : (X : Type u_7) → (Y : Type u_8) → [TopologicalSpace X] → [TopologicalSpace Y] → Type (max u_7 u_8)
-- Mathlib.Tactic.LinearCombinationPrime
Mathlib.Tactic.LinearCombinationPrime.c_div_pf : ∀ {α : Type u_1} {b c : α} [inst : Div α], b = c → ∀ (a : α), a / b = a / c
-- Init.Data.UInt.Lemmas
UInt16.toUInt64_ofNatTruncate_of_le : ∀ {n : ℕ},
  UInt16.size ≤ n →
    (UInt16.ofNatClamp n).toUInt64 = UInt64.ofNatLT (UInt16.size - 1) UInt16.toUInt64_ofNatClamp_of_le._proof_1
-- Mathlib.Analysis.RCLike.Basic
/-- The real part as an additive monoid homomorphism  -/
RCLike.re : {K : semiOutParam (Type u_1)} → [self : RCLike K] → K →+ ℝ
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- The logarithmic counting function `logCounting f 0` is the logarithmic counting function associated
with the zero-divisor of `f`.
 -/
ValueDistribution.logCounting_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : 𝕜 → E},
  ValueDistribution.logCounting f 0 = Function.locallyFinsuppWithin.logCounting (MeromorphicOn.divisor f Set.univ)⁺
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.RootPositiveForm.mk.sizeOf_spec : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing S]
  [inst_1 : LinearOrder S] [inst_2 : CommRing R] [inst_3 : Algebra S R] [inst_4 : AddCommGroup M] [inst_5 : Module R M]
  [inst_6 : AddCommGroup N] [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsValuedIn S]
  [inst_9 : SizeOf ι] [inst_10 : SizeOf R] [inst_11 : SizeOf S] [inst_12 : SizeOf M] [inst_13 : SizeOf N]
  (form : LinearMap.BilinForm R M) (symm : LinearMap.IsSymm form)
  (isOrthogonal_reflection : ∀ (i : ι), LinearMap.IsOrthogonal form ⇑(P.reflection i))
  (exists_eq : ∀ (i j : ι), ∃ s, (algebraMap S R) s = (form (P.root i)) (P.root j))
  (exists_pos_eq : ∀ (i : ι), ∃ s > 0, (algebraMap S R) s = (form (P.root i)) (P.root i)),
  sizeOf
      { form := form, symm := symm, isOrthogonal_reflection := isOrthogonal_reflection, exists_eq := exists_eq,
        exists_pos_eq := exists_pos_eq } =
    1 + sizeOf form + sizeOf symm
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.contains_eq_isSome_get? : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {a : α}, m.contains a = (m.get? a).isSome
-- Mathlib.LinearAlgebra.Dimension.Finite
/-- See `rank_subsingleton` for the reason that `Nontrivial R` is needed.  -/
Submodule.rank_eq_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M] {S : Submodule R M}, Module.rank R ↥S = 0 ↔ S = ⊥
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.infEDist_le_edist_add_infEDist`. -/
EMetric.infEdist_le_edist_add_infEdist : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {s : Set α},
  Metric.infEDist x s ≤ edist x y + Metric.infEDist y s
-- Init.Data.Array.Monadic
_private.Init.Data.Array.Monadic.0.Array.filterMapM.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match none with
    | some b => h_1 b
    | none => h_2 ()) =
    h_2 ()
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → Type
-- Mathlib.Data.Finset.Fin
Finset.attachFin_ssubset_attachFin : ∀ {n : ℕ} {s t : Finset ℕ} (hst : s ⊂ t) (ht : ∀ m ∈ t, m < n), s.attachFin ⋯ ⊂ t.attachFin ht
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.measure_eq_zero_or_one_or_top_of_indepSet_self : ∀ {Ω : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : Set Ω},
  ProbabilityTheory.IndepSet t t μ → μ t = 0 ∨ μ t = 1 ∨ μ t = ⊤
-- Mathlib.MeasureTheory.Order.Lattice
OrderDual.instMeasurableInf : ∀ {M : Type u_1} [inst : MeasurableSpace M] [inst_1 : Max M] [MeasurableSup M], MeasurableInf Mᵒᵈ
-- Lean.Server.FileWorker.Utils
/-- Creates a new `EditableDocumentCore` for a new document version, sharing the same sticky
diagnostics with the previous version.
 -/
Lean.Server.FileWorker.EditableDocumentCore.update : Lean.Server.FileWorker.EditableDocumentCore →
  Lean.Server.DocumentMeta → Lean.Language.Lean.InitialSnapshot → BaseIO Lean.Server.FileWorker.EditableDocumentCore
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α}
  {k : α}, k ∉ m → l.contains k = false → (m.insertManyIfNewUnit l).getKey? k = none
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int8.reduceToNatClampNeg : Lean.Meta.Simp.DSimproc
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.mk.inj : ∀ {α : Type u_5} {β : Type u_6} {toFun : α → β} {invFun : β → α} {source : Set α} {target : Set β}
  {map_source' : ∀ ⦃x : α⦄, x ∈ source → toFun x ∈ target} {map_target' : ∀ ⦃x : β⦄, x ∈ target → invFun x ∈ source}
  {left_inv' : ∀ ⦃x : α⦄, x ∈ source → invFun (toFun x) = x} {right_inv' : ∀ ⦃x : β⦄, x ∈ target → toFun (invFun x) = x}
  {toFun_1 : α → β} {invFun_1 : β → α} {source_1 : Set α} {target_1 : Set β}
  {map_source'_1 : ∀ ⦃x : α⦄, x ∈ source_1 → toFun_1 x ∈ target_1}
  {map_target'_1 : ∀ ⦃x : β⦄, x ∈ target_1 → invFun_1 x ∈ source_1}
  {left_inv'_1 : ∀ ⦃x : α⦄, x ∈ source_1 → invFun_1 (toFun_1 x) = x}
  {right_inv'_1 : ∀ ⦃x : β⦄, x ∈ target_1 → toFun_1 (invFun_1 x) = x},
  { toFun := toFun, invFun := invFun, source := source, target := target, map_source' := map_source',
        map_target' := map_target', left_inv' := left_inv', right_inv' := right_inv' } =
      { toFun := toFun_1, invFun := invFun_1, source := source_1, target := target_1, map_source' := map_source'_1,
        map_target' := map_target'_1, left_inv' := left_inv'_1, right_inv' := right_inv'_1 } →
    toFun = toFun_1 ∧ invFun = invFun_1 ∧ source = source_1 ∧ target = target_1
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getKeyGED : {α : Type u} → {β : α → Type v} → [Ord α] → α → Std.DTreeMap.Internal.Impl α β → α → α
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
ModelWithCorners.symm.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H), I.symm = I.symm
-- Mathlib.RingTheory.FreeRing
instInhabitedFreeRing : (α : Type u_1) → Inhabited (FreeRing α)
-- Mathlib.Topology.VectorBundle.Basic
instInhabitedVectorBundleCore : (R : Type u_1) →
  (B : Type u_2) →
    (F : Type u_3) →
      [inst : NontriviallyNormedField R] →
        [inst_1 : NormedAddCommGroup F] →
          [inst_2 : NormedSpace R F] →
            [inst_3 : TopologicalSpace B] → (ι : Type u_5) → [Inhabited ι] → Inhabited (VectorBundleCore R B F ι)
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
CategoryTheory.Limits.IsCofiltered.sequentialFunctor_initial : ∀ (J : Type u_2) [inst : Countable J] [inst_1 : Preorder J] [inst_2 : CategoryTheory.IsCofiltered J],
  (CategoryTheory.Limits.IsCofiltered.sequentialFunctor J).Initial
-- Mathlib.Tactic.Simps.Basic
/-- Find the indices of the projections that need to be applied to elaborate `$e.$projName`.
Example: If `e : α ≃+ β` and ``projName = `invFun`` then this returns `[0, 1]`, because the first
projection of `MulEquiv` is `toEquiv` and the second projection of `Equiv` is `invFun`.  -/
Simps.findProjectionIndices : Lean.Name → Lean.Name → Lean.MetaM (List ℕ)
-- Mathlib.LinearAlgebra.BilinearMap
/-- If `B : M → N → Pₗ` is `R`-`S` bilinear and `R'` and `S'` are compatible scalar multiplications,
then the restriction of scalars is a `R'`-`S'` bilinear map.  -/
LinearMap.restrictScalars₁₂ : {R : Type u_1} →
  {S : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        {M : Type u_5} →
          {N : Type u_7} →
            {Pₗ : Type u_11} →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid N] →
                  [inst_4 : AddCommMonoid Pₗ] →
                    [inst_5 : Module R M] →
                      [inst_6 : Module S N] →
                        [inst_7 : Module R Pₗ] →
                          [inst_8 : Module S Pₗ] →
                            [inst_9 : SMulCommClass S R Pₗ] →
                              (R' : Type u_14) →
                                (S' : Type u_15) →
                                  [inst_10 : Semiring R'] →
                                    [inst_11 : Semiring S'] →
                                      [inst_12 : Module R' M] →
                                        [inst_13 : Module S' N] →
                                          [inst_14 : Module R' Pₗ] →
                                            [inst_15 : Module S' Pₗ] →
                                              [inst_16 : SMulCommClass S' R' Pₗ] →
                                                [inst_17 : SMul S' S] →
                                                  [IsScalarTower S' S N] →
                                                    [IsScalarTower S' S Pₗ] →
                                                      [inst_20 : SMul R' R] →
                                                        [IsScalarTower R' R M] →
                                                          [IsScalarTower R' R Pₗ] →
                                                            (M →ₗ[R] N →ₗ[S] Pₗ) → M →ₗ[R'] N →ₗ[S'] Pₗ
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
/-- The sheaf of smooth functions from `M` to `A`, for `A` an abelian Lie group, as a
sheaf of abelian groups.  -/
smoothSheafCommGroup : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              ModelWithCorners 𝕜 EM HM →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          (I : ModelWithCorners 𝕜 E H) →
                            (M : Type u) →
                              [inst_7 : TopologicalSpace M] →
                                [ChartedSpace HM M] →
                                  (A : Type u) →
                                    [inst_9 : TopologicalSpace A] →
                                      [inst_10 : ChartedSpace H A] →
                                        [inst_11 : CommGroup A] →
                                          [LieGroup I (↑⊤) A] → TopCat.Sheaf CommGrpCat (TopCat.of M)
-- Init.Data.Slice.Array.Iterator
/-- Allocates a new array that contains the contents of the subarray.
 -/
Array.ofSubarray : {α : Type u} → Subarray α → Array α