mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
/-- The (Lebesgue) integral of the conditional (Lebesgue) expectation `P⁻[X|mΩ]` over an
`mΩ`-measurable set is equal to the integral of `X` on that set.  -/
MeasureTheory.setLIntegral_condLExp : ∀ {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} (hm : mΩ ≤ mΩ₀) (P : MeasureTheory.Measure Ω)
  [hσ : MeasureTheory.SigmaFinite (P.trim hm)] (X : Ω → ENNReal) {s : Set Ω},
  MeasurableSet s → ∫⁻ (ω : Ω) in s, P⁻[X | mΩ] ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
-- Mathlib.Algebra.Group.Ideal
/-- An additive semigroup ideal is finitely generated if it is generated by a finite
set.

This is defeq to `SubAddAction.FG`, but unfolds more nicely.  -/
AddSemigroupIdeal.FG : {M : Type u_1} → [inst : Add M] → AddSemigroupIdeal M → Prop
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.eventuallyLE_one_mul_atBot : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedMonoid M] {l : Filter α}
  {f g : α → M}, f ≤ᶠ[l] 1 → Filter.Tendsto g l Filter.atBot → Filter.Tendsto (fun x => f x * g x) l Filter.atBot
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Algebra.map_intTraceAux : ∀ {A : Type u_1} {K : Type u_2} {L : Type u_3} {B : Type u_6} [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : Algebra A B] [inst_3 : Field K] [inst_4 : Field L] [inst_5 : Algebra A K] [inst_6 : IsFractionRing A K]
  [inst_7 : Algebra K L] [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : Algebra B L]
  [inst_11 : IsScalarTower A B L] [inst_12 : IsIntegralClosure B A L] [inst_13 : FiniteDimensional K L]
  [inst_14 : IsIntegrallyClosed A] (x : B),
  (algebraMap A K) ((Algebra.intTraceAux A K L B) x) = (Algebra.trace K L) ((algebraMap B L) x)
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
/-- To ease type checking, we also provide a version of inl that lives in
`SimplexCategory`.  -/
AugmentedSimplexCategory.inl' : (x y : SimplexCategory) → x ⟶ AugmentedSimplexCategory.tensorObjOf x y
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_mul_const_left : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (c : ℝ),
  ProbabilityTheory.covariance (fun ω => X ω * c) Y μ = ProbabilityTheory.covariance X Y μ * c
-- Mathlib.Data.Finset.Defs
Finset.val_le_iff : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, s₁.val ≤ s₂.val ↔ s₁ ⊆ s₂
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.algebraMap_apply : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {R : Type u_1} [inst_2 : CommSemiring R]
  [inst_3 : Algebra R (Polynomial K)] (x : R),
  (algebraMap R (RatFunc K)) x =
    (algebraMap (Polynomial K) (RatFunc K)) ((algebraMap R (Polynomial K)) x) /
      (algebraMap (Polynomial K) (RatFunc K)) 1
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.mk_left_unitor_hom : ∀ {B : Type u} [inst : Quiver B] {a b : CategoryTheory.FreeBicategory B} (f : a ⟶ b),
  Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.left_unitor f) =
    (CategoryTheory.Bicategory.leftUnitor f).hom
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_assoc : ∀ {α : Type u_1} [inst : DecidableEq α] (s₁ s₂ s₃ : Finset α), s₁ ∪ s₂ ∪ s₃ = s₁ ∪ (s₂ ∪ s₃)
-- Init.Data.List.Nat.Count
List.IsPrefix.le_countP : ∀ {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool},
  l₁ <+: l₂ → List.countP p l₂ - (l₂.length - l₁.length) ≤ List.countP p l₁
-- Init.Data.SInt.Lemmas
Int64.toBitVec_toInt16 : ∀ (x : Int64), x.toInt16.toBitVec = BitVec.signExtend 16 x.toBitVec
-- Mathlib.Order.CompleteLattice.Finset
Finset.set_biUnion_option_toFinset : ∀ {α : Type u_2} {β : Type u_3} (o : Option α) (f : α → Set β), ⋃ x ∈ o.toFinset, f x = ⋃ x ∈ o, f x
-- Mathlib.Topology.Order
/-- **Alias** of `setOfPred_isOpen_sSup`. -/
setOf_isOpen_sSup : ∀ {α : Type u} {T : Set (TopologicalSpace α)}, {s | IsOpen s} = ⋂ t ∈ T, {s | IsOpen s}
-- Mathlib.RepresentationTheory.Character
Representation.character.eq_1 : ∀ {G : Type u_1} {k : Type u_2} {V : Type u_3} [inst : Monoid G] [inst_1 : Field k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) (g : G), ρ.character g = (LinearMap.trace k V) (ρ g)
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.StronglyAdapted.isStoppingTime_crossing : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n : ℕ} {ℱ : MeasureTheory.Filtration ℕ m0},
  MeasureTheory.StronglyAdapted ℱ f →
    (MeasureTheory.IsStoppingTime ℱ fun ω => ↑(MeasureTheory.upperCrossingTime a b f N n ω)) ∧
      MeasureTheory.IsStoppingTime ℱ fun ω => ↑(MeasureTheory.lowerCrossingTime a b f N n ω)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Sub
MeasureTheory.lintegral_iInf' : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal},
  (∀ (n : ℕ), AEMeasurable (f n) μ) →
    (∀ᵐ (a : α) ∂μ, Antitone fun i => f i a) →
      ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤ → ∫⁻ (a : α), ⨅ n, f n a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instAddCommSemigroupOfContinuousAdd : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : AddCommSemigroup β] → [ContinuousAdd β] → AddCommSemigroup C(α, β)
-- Mathlib.Analysis.InnerProductSpace.Projection.Reflection
/-- The result of reflecting.  -/
Submodule.reflection_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] (p : E), K.reflection p = 2 • K.starProjection p - p
-- Std.Data.HashMap.Lemmas
Std.HashMap.find?_toArray_eq_none_iff_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, Array.find? (fun x_2 => x_2.1 == k) m.toArray = none ↔ m.contains k = false
-- Mathlib.Algebra.Ring.Basic
isDomain_iff_noZeroDivisors_and_nontrivial : ∀ (α : Type u_3) [inst : Ring α], IsDomain α ↔ NoZeroDivisors α ∧ Nontrivial α
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- A cocone precomposed with the inverse of a natural isomorphism is a colimit cocone
if and only if the original cocone is.
 -/
CategoryTheory.Limits.IsColimit.precomposeInvEquiv : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F G : CategoryTheory.Functor J C} →
          (α : F ≅ G) →
            (c : CategoryTheory.Limits.Cocone F) →
              CategoryTheory.Limits.IsColimit ((CategoryTheory.Limits.Cocone.precompose α.inv).obj c) ≃
                CategoryTheory.Limits.IsColimit c
-- Mathlib.NumberTheory.NumberField.House
NumberField.house.basis_repr_norm_le_const_mul_house : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] [inst_2 : DecidableEq (K →+* ℂ)]
  (α : NumberField.RingOfIntegers K) (i : K →+* ℂ),
  ‖↑((((NumberField.integralBasis K).reindex (NumberField.equivReindex K).symm).repr ↑α) i)‖ ≤
    NumberField.house.c✝ K * NumberField.house ((algebraMap (NumberField.RingOfIntegers K) K) α)
-- Batteries.Data.List.Perm
List.getD_set_perm_cons : ∀ {α : Type u_1} (xs : List α) (i : ℕ) (v : α), (xs[i]?.getD v :: xs.set i v).Perm (v :: xs)
-- Mathlib.Probability.CDF
/-- The cdf is lower or equal to 1.  -/
ProbabilityTheory.cdf_le_one : ∀ (μ : MeasureTheory.Measure ℝ) (x : ℝ), ↑(ProbabilityTheory.cdf μ) x ≤ 1
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrpObj.neg_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H X : C} [inst_2 : CategoryTheory.AddGrpObj G] [inst_3 : CategoryTheory.AddGrpObj H] (f : X ⟶ G) (g : G ⟶ H)
  [CategoryTheory.IsAddMonHom g] {Z : C} (h : H ⟶ Z),
  CategoryTheory.CategoryStruct.comp (-f) (CategoryTheory.CategoryStruct.comp g h) =
    CategoryTheory.CategoryStruct.comp (-CategoryTheory.CategoryStruct.comp f g) h
-- ProofWidgets.Util
/-- Sends `#[a, b, c]` to `` `(term| $a ++ $b ++ $c)`` -/
ProofWidgets.Util.joinArrays : {m : Type → Type} → [Monad m] → [Lean.MonadRef m] → [Lean.MonadQuotation m] → Array Lean.Term → m Lean.Term
-- Mathlib.Data.Sigma.Basic
Sigma.fst_injective : ∀ {α : Type u_1} {β : α → Type u_4} [h : ∀ (a : α), Subsingleton (β a)], Function.Injective Sigma.fst
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_zero : ∀ (R : Type u_1) {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] (a : A), cfcₙ 0 a = 0
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.mk'X_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C) [inst_3 : CategoryTheory.BimonObj X],
  (CategoryTheory.Bimon.mk'X X).X = X
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.NormalizePattern.State.bvarsFound : Lean.Meta.Grind.NormalizePattern.State → Std.HashSet ℕ
-- Mathlib.Data.List.TakeDrop
List.span_eq_takeWhile_dropWhile : ∀ {α : Type u} (p : α → Bool) (l : List α), List.span p l = (List.takeWhile p l, List.dropWhile p l)
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.nonempty_iff : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens), Nonempty ↥↑U ↔ (↑U).Nonempty
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubgroup.sSup_normal : ∀ {G : Type u_2} [inst : AddGroup G] (Hs : Set (AddSubgroup G)), (∀ H ∈ Hs, H.Normal) → (sSup Hs).Normal
-- Plausible.Functions
/-- Implementation of `Repr (TotalFunction α β)`.

Creates a string for a given `Finmap` and output, `x₀ => y₀, .. xₙ => yₙ`
for each of the entries. The brackets are provided by the calling function.
 -/
Plausible.TotalFunction.reprAux : {α : Type u} → {β : Type v} → [Repr α] → [Repr β] → List ((_ : α) × β) → String
-- Lean.Data.Options
Lean.getBoolOption : {m : Type → Type} → [Monad m] → [Lean.MonadOptions m] → Lean.Name → optParam Bool false → m Bool
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.isLocal_reflectionObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} (Z : C)
  [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_3 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂]
  [inst_4 :
    ∀ (Z : C), CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)]
  {κ : Cardinal.{w}} [inst_5 : OrderBot κ.ord.ToType]
  [inst_6 : CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C] [inst_7 : Fact κ.IsRegular],
  (∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → CategoryTheory.IsCardinalPresentable X κ ∧ CategoryTheory.IsCardinalPresentable Y κ) →
    W.isLocal (CategoryTheory.OrthogonalReflection.reflectionObj W Z κ)
-- Init.Meta.Defs
Lean.Internal.isStage0 : Unit → Bool
-- Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {H : J.OneHypercoverFamily} {P : CategoryTheory.Functor Cᵒᵖ A}
  (hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (CategoryTheory.Limits.IsLimit (E.multifork P))) {X : C}
  {S : CategoryTheory.Sieve X} {E : J.OneHypercover X} (hE : H E) (le : E.sieve₀ ≤ S)
  (F : CategoryTheory.Limits.Multifork (CategoryTheory.GrothendieckTopology.Cover.index ⟨S, ⋯⟩ P)) [H.IsGenerating]
  {Y : C} (f : Y ⟶ X) (hf : S.arrows f),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.lift hP hE le F) (P.map f.op) =
    F.ι { Y := Y, f := f, hf := hf }
-- Std.Async.Process
/-- Gets the current working directory.
 -/
Std.IO.Process.getCwd : IO System.FilePath
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.isAlgebraic_root : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R}, f ≠ 0 → IsAlgebraic R (AdjoinRoot.root f)
-- Mathlib.Topology.ContinuousMap.CompactlySupported
/-- Pull back a continuous compactly supported function `f` on `β` along a closed
embedding `φ : α →+ β` to the continuous compactly supported function `a ↦ f (b + φ a)` on `A`.  -/
CompactlySupportedContinuousMap.pullback_addMonoidHom : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : TopologicalSpace α] →
        [R1Space α] →
          [inst_2 : AddGroup α] →
            [inst_3 : TopologicalSpace β] →
              [R1Space β] →
                [inst_5 : AddGroup β] →
                  [ContinuousAdd β] →
                    [inst_7 : NormedAddCommGroup γ] →
                      {φ : α →+ β} →
                        Topology.IsClosedEmbedding ⇑φ →
                          CompactlySupportedContinuousMap β γ → β → CompactlySupportedContinuousMap α γ
-- Init.Prelude
/-- Function that tries to reverse macro expansions as a post-processing step of delaboration.
While less general than an arbitrary delaborator, it can be declared without importing `Lean`.
Used by the `[app_unexpander]` attribute.
 -/
Lean.PrettyPrinter.Unexpander : Type
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_mul_iff_one_lt_right' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LT α] [MulLeftStrictMono α] [MulLeftReflectLT α] (a : α) {b : α},
  a < a * b ↔ 1 < b
-- Std.Data.TreeSet.Raw.Basic
Std.TreeSet.Raw.mk.injEq : ∀ {α : Type u} {cmp : autoParam (α → α → Ordering) Std.TreeSet.Raw._auto_1}
  (inner inner_1 : Std.TreeMap.Raw α Unit cmp), ({ inner := inner } = { inner := inner_1 }) = (inner = inner_1)
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedLinearMap.smul : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] {f : E → F} {𝕜' : Type u_5} (c : 𝕜')
  [inst_5 : SeminormedRing 𝕜'] [inst_6 : Module 𝕜' F] [IsBoundedSMul 𝕜' F] [SMulCommClass 𝕜 𝕜' F],
  IsBoundedLinearMap 𝕜 f → IsBoundedLinearMap 𝕜 (c • f)
-- Init.Data.String.Basic
String.Pos.lt_of_le_of_ne : ∀ {s : String} {p q : s.Pos}, p ≤ q → p ≠ q → p < q
-- Mathlib.GroupTheory.Solvable
derivedSeries_one : ∀ (G : Type u_1) [inst : Group G], derivedSeries G 1 = commutator G
-- Init.Notation
/-- Precedence used for application arguments (`do`, `by`, ...).  -/
precArg : Lean.ParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- A graph is preconnected if every pair of vertices is reachable from one another.  -/
SimpleGraph.Preconnected : {V : Type u} → SimpleGraph V → Prop
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min!_le_min!_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  (t.erase k).isEmpty = false → (cmp t.min! (t.erase k).min!).isLE = true
-- Mathlib.Data.EReal.Inv
EReal.instPosMulReflectLT : PosMulReflectLT EReal
-- Mathlib.Order.Interval.Basic
/-- Pushforward of nonempty intervals.  -/
NonemptyInterval.map : {α : Type u_1} →
  {β : Type u_2} → [inst : Preorder α] → [inst_1 : Preorder β] → (α →o β) → NonemptyInterval α → NonemptyInterval β
-- Mathlib.FieldTheory.RatFunc.Defs
RatFunc.mk.congr_simp : ∀ {K : Type u_1} [inst : CommRing K] [inst_1 : IsDomain K] (p p_1 : Polynomial K),
  p = p_1 → ∀ (q q_1 : Polynomial K), q = q_1 → RatFunc.mk p q = RatFunc.mk p_1 q_1
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `DifferentiableOn.sub` -/
DifferentiableOn.fun_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {s : Set E}, DifferentiableOn 𝕜 f s → DifferentiableOn 𝕜 g s → DifferentiableOn 𝕜 (fun i => f i - g i) s
-- Mathlib.Geometry.Manifold.Notation
/-- `MDiffAt[s] f x` elaborates to `MDifferentiableWithinAt I J f s x`,
trying to determine `I` and `J` from the local context.
The argument `x` can be omitted.  -/
Manifold.«termMDiffAt[_]__» : Lean.ParserDescr
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- Reinterpret an `AffineEquiv` as an `AffineMap`.  -/
AffineEquiv.toAffineMap : {k : Type u_1} →
  {P₁ : Type u_2} →
    {P₂ : Type u_3} →
      {V₁ : Type u_6} →
        {V₂ : Type u_7} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [inst_2 : AddCommGroup V₂] →
                [inst_3 : Module k V₁] →
                  [inst_4 : Module k V₂] →
                    [inst_5 : AddTorsor V₁ P₁] → [inst_6 : AddTorsor V₂ P₂] → (P₁ ≃ᵃ[k] P₂) → P₁ →ᵃ[k] P₂
-- Mathlib.LinearAlgebra.Projection
LinearMap.IsProj.submodule_unique : ∀ {S : Type u_5} [inst : Semiring S] {M : Type u_6} [inst_1 : AddCommMonoid M] [inst_2 : Module S M] {f : M →ₗ[S] M}
  {m₁ m₂ : Submodule S M}, LinearMap.IsProj m₁ f → LinearMap.IsProj m₂ f → m₁ = m₂
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getThenInsertIfNew?_fst : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {v : β}, (Std.ExtDTreeMap.Const.getThenInsertIfNew? t k v).1 = Std.ExtDTreeMap.Const.get? t k
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Alt.brecOn_2.go : {pu : Lean.Compiler.LCNF.Purity} →
  {motive_1 : Lean.Compiler.LCNF.Alt pu → Sort u} →
    {motive_2 : Lean.Compiler.LCNF.FunDecl pu → Sort u} →
      {motive_3 : Lean.Compiler.LCNF.Cases pu → Sort u} →
        {motive_4 : Lean.Compiler.LCNF.Code pu → Sort u} →
          {motive_5 : Array (Lean.Compiler.LCNF.Alt pu) → Sort u} →
            {motive_6 : List (Lean.Compiler.LCNF.Alt pu) → Sort u} →
              (t : List (Lean.Compiler.LCNF.Alt pu)) →
                ((t : Lean.Compiler.LCNF.Alt pu) → t.below → motive_1 t) →
                  ((t : Lean.Compiler.LCNF.FunDecl pu) → t.below → motive_2 t) →
                    ((t : Lean.Compiler.LCNF.Cases pu) → t.below → motive_3 t) →
                      ((t : Lean.Compiler.LCNF.Code pu) → t.below → motive_4 t) →
                        ((t : Array (Lean.Compiler.LCNF.Alt pu)) → Lean.Compiler.LCNF.Alt.below_1 t → motive_5 t) →
                          ((t : List (Lean.Compiler.LCNF.Alt pu)) → Lean.Compiler.LCNF.Alt.below_2 t → motive_6 t) →
                            motive_6 t ×' Lean.Compiler.LCNF.Alt.below_2 t
-- Mathlib.Data.Vector.Basic
/-- Define `C u v w` by induction on a triplet of vectors
`u : Vector α n`, `v : Vector β n`, and `w : Vector γ b`.  -/
List.Vector.inductionOn₃ : {α : Type u_1} →
  {n : ℕ} →
    {β : Type u_6} →
      {γ : Type u_7} →
        {C : {n : ℕ} → List.Vector α n → List.Vector β n → List.Vector γ n → Sort u_8} →
          (u : List.Vector α n) →
            (v : List.Vector β n) →
              (w : List.Vector γ n) →
                C List.Vector.nil List.Vector.nil List.Vector.nil →
                  ({n : ℕ} →
                      {a : α} →
                        {b : β} →
                          {c : γ} →
                            {x : List.Vector α n} →
                              {y : List.Vector β n} →
                                {z : List.Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)) →
                    C u v w
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Stream'.WSeq.destruct.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option (Stream'.Seq1 (Option α)) → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (s' : Stream'.Seq (Option α)) → motive (some (none, s')))
  (h_3 : (a : α) → (s' : Stream'.Seq (Option α)) → motive (some (some a, s'))),
  (match none with
    | none => h_1 ()
    | some (none, s') => h_2 s'
    | some (some a, s') => h_3 a s') =
    h_1 ()
-- Mathlib.CategoryTheory.Sites.CoversTop.Basic
CategoryTheory.GrothendieckTopology.CoversTop.sections_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {I : Type u_1}
  {Y : I → C},
  J.CoversTop Y →
    ∀ (F : CategoryTheory.Sheaf J (Type u_2)) {x y : ↑F.obj.sections},
      (∀ (i : I), ↑x (Opposite.op (Y i)) = ↑y (Opposite.op (Y i))) → x = y
-- Aesop.Options.Public
/-- Breadth-first search. Aesop always works on the oldest unsolved goal. Goal and
rule priorities are ignored, except to decide which rule is applied first.
 -/
Aesop.Strategy.breadthFirst : Aesop.Strategy
-- Mathlib.Algebra.Group.Action.Defs
/-- Typeclass for multiplicative actions on multiplicative structures.

The key axiom here is `smul_mul : g • (x * y) = (g • x) * (g • y)`.
If `G` is a multiplicative group with automorphism group `Γ`, then there is a natural instance of
`MulDistribMulAction Γ G`.

The axiom is also satisfied by a Galois group $Gal(L/K)$ acting on the field `L`,
but here you can use the even stronger class `MulSemiringAction`, which captures
how the action plays with both multiplication and addition.  -/
MulDistribMulAction : (M : Type u_9) → (N : Type u_10) → [Monoid M] → [Monoid N] → Type (max u_10 u_9)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.setLIntegral_le_lintegral : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α) (f : α → ENNReal),
  ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
-- Mathlib.Topology.UniformSpace.Cauchy
SequentiallyComplete.setSeq_prod_subset : ∀ {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α}
  (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) {N m n : ℕ},
  N ≤ m → N ≤ n → SequentiallyComplete.setSeq hf U_mem m ×ˢ SequentiallyComplete.setSeq hf U_mem n ⊆ U N
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
cfcₙL.congr_simp : ∀ {R : Type u_1} {A : Type u_2} {p p_1 : A → Prop} (e_p : p = p_1) [inst : CommSemiring R] [inst_1 : Nontrivial R]
  [inst_2 : StarRing R] [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R]
  [inst_6 : NonUnitalRing A] [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A]
  [inst_10 : IsScalarTower R A A] [inst_11 : SMulCommClass R A A]
  [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {a : A} (ha : p a), cfcₙL ha = cfcₙL ⋯
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex_ι : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.rightHomologyDataShortComplex._auto_3),
  (X.rightHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).ι =
    CategoryTheory.Limits.kernel.ι (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ ⋯)
-- Mathlib.Algebra.Category.ModuleCat.Basic
/-- Turn a homomorphism into a bilinear map.  -/
ModuleCat.Hom.hom₂ : {R : Type u_1} → [inst : CommRing R] → {M N P : ModuleCat R} → (M ⟶ ModuleCat.of R (N ⟶ P)) → ↑M →ₗ[R] ↑N →ₗ[R] ↑P
-- Lean.Elab.Term.TermElabM
/-- Log the given exception, and create a synthetic sorry for representing the failed
elaboration step with exception `ex`.
 -/
Lean.Elab.Term.exceptionToSorry : Lean.Exception → Option Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.instSMulCommClassCircle : SMulCommClass Circle Complex.UnitClosedDisc Complex.UnitClosedDisc
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_primeCompl_comap_of_surjective : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [inst_3 : RingHomClass F R S],
  Function.Surjective ⇑f →
    ∀ (p : Ideal S) [inst_4 : p.IsPrime], Submonoid.map f (Ideal.comap f p).primeCompl = p.primeCompl