mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.IsometricSMul
ediam_smul : ∀ {M : Type u} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : SMul M X] [IsIsometricSMul M X] (c : M) (s : Set X),
  Metric.ediam (c • s) = Metric.ediam s
-- Mathlib.Data.Finset.Lattice.Lemmas
Finset.insert_union_distrib : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s t : Finset α), insert a (s ∪ t) = insert a s ∪ insert a t
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.inr_map_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {W X Y Z : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct W X]
  [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {Z_1 : C} (h : Y ⊞ Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f g) h) =
    CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr h)
-- Mathlib.Algebra.AddConstMap.Equiv
/-- Interpret an `AddConstEquiv` as an `AddConstMap`.  -/
AddConstEquiv.toAddConstMap : {G : Type u_1} →
  {H : Type u_2} → [inst : Add G] → [inst_1 : Add H] → {a : G} → {b : H} → AddConstEquiv G H a b → AddConstMap G H a b
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
/-- Global root number of `χ` (for `χ` primitive; junk otherwise). Defined as
`gaussSum χ stdAddChar / I ^ a / N ^ (1 / 2)`, where `a = 0` if even, `a = 1` if odd. (The factor
`1 / I ^ a` is the Archimedean root number.) This is a complex number of absolute value 1.
 -/
DirichletCharacter.rootNumber : {N : ℕ} → [NeZero N] → DirichletCharacter ℂ N → ℂ
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_insertList_of_contains_right_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : Inhabited α] [inst_1 : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)}
  {k : α},
  Std.Internal.List.containsKey k toInsert = false →
    Std.Internal.List.getKey! k (Std.Internal.List.insertList l toInsert) = Std.Internal.List.getKey! k l
-- Init.Data.Option.Attach
Option.instMonadAttach : MonadAttach Option
-- Batteries.Control.ForInStep.Lemmas
ForInStep.bind_yield_bindList : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : α → β → m (ForInStep β))
  (s : ForInStep β) (l : List α),
  (s.bind fun a => ForInStep.bindList f l (ForInStep.yield a)) = ForInStep.bindList f l s
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_set_MonadStateOf_lift_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m n : Type u → Type v} [inst : MonadLift m n]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : (α : Type u) → Std.Internal.Do.WP (n α) α Pred EPred] {σ : Type u} {post : PUnit.{u + 1} → Pred}
  {epost : EPred} [inst_4 : MonadStateOf σ m] (x : σ),
  Std.Internal.Do.wp (set x) post epost = Std.Internal.Do.wp (MonadLift.monadLift (set x)) post epost
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.prodComm_symm : ∀ (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 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂],
  (ContinuousAffineEquiv.prodComm k P₁ P₂).symm = ContinuousAffineEquiv.prodComm k P₂ P₁
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.untopD_zero_mul : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] (a b : WithTop α),
  WithTop.untopD 0 (a * b) = WithTop.untopD 0 a * WithTop.untopD 0 b
-- Init.Data.List.ToArray
List.findRevM?_toArray : ∀ {m : Type → Type u_1} {α : Type} [inst : Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α),
  Array.findRevM? f l.toArray = List.findM? f l.reverse
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.coe_singleton : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : MeasurableSingletonClass α] (a : α), ↑{a} = {a}
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_ofNat : ∀ (x : NNReal) (n : ℕ) [inst : n.AtLeastTwo], x ^ OfNat.ofNat n = x ^ OfNat.ofNat n
-- Mathlib.Data.ENat.Pow
ENat.epow_def : ∀ {x y : ℕ∞}, x ^ y = if y < ⊤ then x ^ y.toNat else if x = 0 then 0 else if x = 1 then 1 else ⊤
-- Init.Grind.AC
Lean.Grind.AC.eq_simp_lhs_suffix : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op}
  (lhs₁ rhs₁ head lhs₂ rhs₂ lhs₂' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.simp_suffix_cert lhs₁ rhs₁ head lhs₂ lhs₂' = true →
    Lean.Grind.AC.Seq.denote ctx lhs₁ = Lean.Grind.AC.Seq.denote ctx rhs₁ →
      Lean.Grind.AC.Seq.denote ctx lhs₂ = Lean.Grind.AC.Seq.denote ctx rhs₂ →
        Lean.Grind.AC.Seq.denote ctx lhs₂' = Lean.Grind.AC.Seq.denote ctx rhs₂
-- Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
/-- A presieve is effective epimorphic if the cocone associated to the sieve it generates
is a colimit cocone.  -/
CategoryTheory.Presieve.EffectiveEpimorphic : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X : C} → CategoryTheory.Presieve X → Prop
-- Std.Http.Protocol.H1.Config
/-- Maximum number of trailer headers (default: 20).
 -/
Std.Http.Protocol.H1.Config.maxTrailerHeaders : Std.Http.Protocol.H1.Config → ℕ
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- **Alias** of `sum_apply`. -/
MultilinearMap.sum_apply : ∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} {ι : Type u_11} [inst : FunLike F α β] [inst_1 : AddCommMonoid β]
  [inst_2 : AddCommMonoid F] [IsZeroApply F α β] [IsAddApply F α β] (s : Finset ι) (f : ι → F) (x : α),
  (∑ i ∈ s, f i) x = ∑ i ∈ s, (f i) x
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsBigOTVS.exists_eventuallyLE : ∀ {𝕜 : Type u_1} {α : Type u_2} {E : Type u_3} {F : Type u_4} [inst : ENorm 𝕜] [inst_1 : TopologicalSpace E]
  [inst_2 : TopologicalSpace F] [inst_3 : Zero E] [inst_4 : Zero F] [inst_5 : SMul 𝕜 E] [inst_6 : SMul 𝕜 F]
  {l : Filter α} {f : α → E} {g : α → F},
  f =O[𝕜; l] g → ∀ U ∈ nhds 0, ∃ V ∈ nhds 0, (fun x => egauge 𝕜 U (f x)) ≤ᶠ[l] fun x => egauge 𝕜 V (g x)
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_succ_succ : ∀ (n k : ℕ), n.succ.choose k.succ = n.choose k + n.choose k.succ
-- Mathlib.Order.Basic
lt_iff_le_and_ne : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, a < b ↔ a ≤ b ∧ a ≠ b
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.instIsWellFoundedMem : IsWellFounded ZFSet.{u_1} fun x1 x2 => x1 ∈ x2
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.congr_apply : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  {S : Type u_3} [inst_2 : Ring S] {Λ₀ : Type u_4} [inst_3 : LinearOrderedCommGroupWithZero Λ₀] (w : Valuation S Λ₀)
  (f : R ≃+* S) (x : WithVal v), (WithVal.congr v w f) x = WithVal.toVal w (f x.ofVal)
-- Lean.CoreM
Lean.Core.instInhabitedCoreM : {α : Type} → Inhabited (Lean.CoreM α)
-- Lean.Parser.Command
Lean.Parser.Command.eraseAttr.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Tactic.ClickSuggestions.Rewrite
/-- Return the rewrite tactic that performs the rewrite.  -/
_private.Mathlib.Tactic.ClickSuggestions.Rewrite.0.Mathlib.Tactic.ClickSuggestions.tacticSyntax : Mathlib.Tactic.ClickSuggestions.RwLemma →
  Mathlib.Tactic.ClickSuggestions.RwKind → Option Lean.Ident → Lean.Expr → Bool → Lean.MetaM (Lean.TSyntax `tactic)
-- Mathlib.Algebra.Group.ULift
ULift.neg : {α : Type u} → [Neg α] → Neg (ULift.{u_1, u} α)
-- Lean.Level
Lean.Level.instBEq : BEq Lean.Level
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
FreeSimplexQuiver.Hom.σ.injEq : ∀ {n : ℕ} (i i_1 : Fin (n + 1)), (FreeSimplexQuiver.Hom.σ i = FreeSimplexQuiver.Hom.σ i_1) = (i = i_1)
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.of_intermediateField : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [NumberField K] [NumberField L]
  [inst_4 : Algebra K L] (E : IntermediateField K L), NumberField ↥E
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
/-- **Alias** of `MeasureTheory.integral_finsetSum`. -/
MeasureTheory.integral_finset_sum : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {ι : Type u_6} (s : Finset ι) {f : ι → α → G},
  (∀ i ∈ s, MeasureTheory.Integrable (f i) μ) → ∫ (a : α), ∑ i ∈ s, f i a ∂μ = ∑ i ∈ s, ∫ (a : α), f i a ∂μ
-- Mathlib.Analysis.Fourier.Notation
FourierModule.mk.sizeOf_spec : ∀ {R : Type u_5} {E : Type u_6} {F : outParam (Type u_7)} [inst : Add E] [inst_1 : Add F] [inst_2 : SMul R E]
  [inst_3 : SMul R F] [inst_4 : SizeOf R] [inst_5 : SizeOf E] [inst_6 : SizeOf F]
  (toFourierTransform : FourierTransform E F)
  (fourier_add :
    ∀ (f g : E), FourierTransform.fourier (f + g) = FourierTransform.fourier f + FourierTransform.fourier g)
  (fourier_smul : ∀ (r : R) (f : E), FourierTransform.fourier (r • f) = r • FourierTransform.fourier f),
  sizeOf { toFourierTransform := toFourierTransform, fourier_add := fourier_add, fourier_smul := fourier_smul } =
    1 + sizeOf toFourierTransform
-- Mathlib.Analysis.Calculus.FDeriv.Basic
differentiableWithinAt_inter' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s t : Set E},
  t ∈ nhdsWithin x s → (DifferentiableWithinAt 𝕜 f (s ∩ t) x ↔ DifferentiableWithinAt 𝕜 f s x)
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectralRadius.eq_1 : ∀ (𝕜 : Type u_1) {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] (a : A),
  spectralRadius 𝕜 a = ⨆ k ∈ spectrum 𝕜 a, ↑‖k‖₊
-- Init.Data.UInt.Lemmas
USize.mul_comm : ∀ (a b : USize), a * b = b * a
-- Mathlib.RingTheory.Morita.Basic
IsMoritaEquivalent.mk : ∀ {R : Type u₀} [inst : CommSemiring R] {A : Type u₁} [inst_1 : Ring A] [inst_2 : Algebra R A] {B : Type u₂}
  [inst_3 : Ring B] [inst_4 : Algebra R B], Nonempty (MoritaEquivalence R A B) → IsMoritaEquivalent R A B
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_eq_some_getElem!_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {a : α}, t.contains a = true → t[a]? = some t[a]!
-- Mathlib.Data.Finsupp.Defs
Finsupp.ext_iff' : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] {f g : α →₀ M},
  f = g ↔ f.support = g.support ∧ ∀ x ∈ f.support, f x = g x
-- Init.Data.List.Lemmas
List.flatMap_id : ∀ {α : Type u_1} {L : List (List α)}, List.flatMap id L = L.flatten
-- Mathlib.Order.Cofinal
BddAbove.of_not_isCofinal : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α}, ¬IsCofinal s → BddAbove s
-- Mathlib.CategoryTheory.Category.Cat.Op
CategoryTheory.Cat.opFunctorInvolutive_hom_app_toFunctor_obj : ∀ (X : CategoryTheory.Cat) (X_1 : (↑X)ᵒᵖᵒᵖ),
  (CategoryTheory.Cat.opFunctorInvolutive.hom.app X).toFunctor.obj X_1 = Opposite.unop (Opposite.unop X_1)
-- Mathlib.Analysis.Calculus.FDeriv.Add
Differentiable.sub_const : ∀ {𝕜 : 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 : E → F},
  Differentiable 𝕜 f → ∀ (c : F), Differentiable 𝕜 fun y => f y - c
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.instIsIsoMapFunctorOppositePresheafFiberToSheafify : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (P : CategoryTheory.Functor Cᵒᵖ A)
  [inst_4 : CategoryTheory.HasWeakSheafify J A],
  CategoryTheory.IsIso (Φ.presheafFiber.map (CategoryTheory.toSheafify J P))
-- Mathlib.Data.Fin.Tuple.Reflection
FinVec.Forall.eq_1 : ∀ {α : Type u_1} (P : (Fin 0 → α) → Prop), FinVec.Forall P = P ![]
-- Mathlib.Algebra.Order.Ring.Abs
abs_le_iff_mul_self_le : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α}, |a| ≤ |b| ↔ a * a ≤ b * b
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_3.eq_2 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_2 it' h
-- Init.Data.Nat.Basic
Nat.default_eq_zero : default = 0
-- Mathlib.Algebra.GroupWithZero.Action.Basic
DistribMulAction.toAddAut_apply : ∀ (G : Type u_1) (A : Type u_3) [inst : Group G] [inst_1 : AddMonoid A] [inst_2 : DistribMulAction G A] (x : G),
  (DistribMulAction.toAddAut G A) x = DistribMulAction.toAddEquiv A x
-- Mathlib.Analysis.Complex.Schwarz
/-- An auxiliary lemma for `Complex.dist_le_mul_div_pow_of_mapsTo_ball_of_isLittleO`.  -/
_private.Mathlib.Analysis.Complex.Schwarz.0.Complex.schwarz_aux : ∀ {f : ℂ → ℂ} {c z : ℂ} {R₁ R₂ : ℝ} {n : ℕ},
  DifferentiableOn ℂ f (Metric.ball c R₁) →
    Set.MapsTo f (Metric.ball c R₁) (Metric.closedBall (f c) R₂) →
      ((fun x => f x - f c) =o[nhds c] fun w => (w - c) ^ n) →
        z ∈ Metric.ball c R₁ → ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
-- Mathlib.Order.PrimeIdeal
Order.Ideal.IsPrime.compl_mem_of_notMem : ∀ {P : Type u_1} [inst : BooleanAlgebra P] {x : P} {I : Order.Ideal P}, I.IsPrime → x ∉ I → xᶜ ∈ I
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithTerminal.liftFromOverComp_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {X : C}
  {K : CategoryTheory.Functor J (CategoryTheory.Over X)} {F : CategoryTheory.Functor C D}
  (x : CategoryTheory.WithTerminal J),
  CategoryTheory.WithTerminal.liftFromOverComp.inv.app x =
    match x with
    | CategoryTheory.WithTerminal.star =>
      CategoryTheory.CategoryStruct.id
        (((CategoryTheory.WithTerminal.liftFromOver.obj K).comp F).obj CategoryTheory.WithTerminal.star)
    | CategoryTheory.WithTerminal.of a =>
      CategoryTheory.CategoryStruct.id
        (((CategoryTheory.WithTerminal.liftFromOver.obj K).comp F).obj (CategoryTheory.WithTerminal.of a))
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthSup_sup : ∀ {u v : ℕ → EReal},
  LinearGrowth.linearGrowthSup (u ⊔ v) = max (LinearGrowth.linearGrowthSup u) (LinearGrowth.linearGrowthSup v)
-- Mathlib.Analysis.Normed.Group.Defs
NormedGroup.ofSeparation.eq_1 : ∀ {E : Type u_5} [inst : SeminormedGroup E] (h : ∀ (x : E), ‖x‖ = 0 → x = 1),
  NormedGroup.ofSeparation h =
    { toNorm := inst.toNorm, toGroup := inst.toGroup, toPseudoMetricSpace := inst.toPseudoMetricSpace,
      eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
-- Mathlib.Order.Filter.CountableInter
/-- **Alias** of `Filter.EventuallyLE.countable_iUnion`. -/
EventuallyLE.countable_iUnion : ∀ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [CountableInterFilter l] [Countable ι] {s t : ι → Set α},
  (∀ (i : ι), s i ≤ᶠ[l] t i) → ⋃ i, s i ≤ᶠ[l] ⋃ i, t i
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.inclLift_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x ⟶ Z)
  (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) (x : C),
  (CategoryTheory.WithTerminal.inclLift F M hM).inv.app x = CategoryTheory.CategoryStruct.id (F.obj x)
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.face_le_face_iff : ∀ {n : ℕ} (S₁ S₂ : Finset (Fin (n + 1))), SSet.stdSimplex.face S₁ ≤ SSet.stdSimplex.face S₂ ↔ S₁ ⊆ S₂
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.eqToHom_app : ∀ {C D : CategoryTheory.Cat} (F G : C ⟶ D) (h : F = G) (X : ↑C),
  (CategoryTheory.eqToHom h).toNatTrans.app X = CategoryTheory.eqToHom ⋯
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndep_iff_condIndepSets : ∀ {Ω : Type u_1} (m' m₁ m₂ : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] (hm' : m' ≤ mΩ)
  (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.CondIndep m' m₁ m₂ hm' μ ↔
    ProbabilityTheory.CondIndepSets m' hm' {s | MeasurableSet s} {s | MeasurableSet s} μ
-- Mathlib.Tactic.CancelDenoms.Core
/-- `cancel_denoms` attempts to remove numerals from the denominators of fractions.
It works on propositions that are field-valued inequalities.

```lean
variable [LinearOrderedField α] (a b c : α)

example (h : a / 5 + b / 4 < c) : 4*a + 5*b < 20*c := by
  cancel_denoms at h
  exact h

example (h : a > 0) : a / 5 > 0 := by
  cancel_denoms
  exact h
```
 -/
Mathlib.Tactic.tacticCancel_denoms_ : Lean.ParserDescr
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.curryRingEquiv_symm_single : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : Monoid M] [inst_2 : Monoid N] (m : M)
  (n : N) (r : R),
  MonoidAlgebra.curryRingEquiv.symm (MonoidAlgebra.single m (MonoidAlgebra.single n r)) = MonoidAlgebra.single (m, n) r
-- Mathlib.Algebra.Algebra.Operations
/-- Dependent version of `Submodule.smul_induction_on`.  -/
Submodule.smul_induction_on' : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A] {M : Type u_1}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M]
  {I : Submodule R A} {N : Submodule R M} {x : M} (hx : x ∈ I • N) {p : (x : M) → x ∈ I • N → Prop},
  (∀ (r : A) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) ⋯) →
    (∀ (x : M) (hx : x ∈ I • N) (y : M) (hy : y ∈ I • N), p x hx → p y hy → p (x + y) ⋯) → p x hx
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- In a balanced category, if a short complex `S` is exact and `S.f` is a mono, then
`S.X₁` is the kernel of `S.g`.  -/
CategoryTheory.ShortComplex.Exact.fIsKernel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S : CategoryTheory.ShortComplex C} →
        [CategoryTheory.Balanced C] →
          S.Exact →
            [CategoryTheory.Mono S.f] → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι S.f ⋯)
-- Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
/-- Two Gaussian processes $(X_s)_{s \in S}$ and $(Y_t)_{t \in T}$ that are jointly Gaussian
are independent if for all $s \in S$ and $t \in T$, $X_s$ and $Y_t$ are uncorrelated.  -/
ProbabilityTheory.IsGaussianProcess.indepFun_of_covariance_inner : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
  [CompleteSpace E] {S : Type u_4} {X : S → Ω → E} {Y : T → Ω → E} [inst_5 : InnerProductSpace ℝ E],
  ProbabilityTheory.IsGaussianProcess (Sum.elim X Y) P →
    (∀ (s : S), AEMeasurable (X s) P) →
      (∀ (t : T), AEMeasurable (Y t) P) →
        (∀ (s : S) (t : T) (x y : E),
            ProbabilityTheory.covariance (fun ω => inner ℝ x (X s ω)) (fun ω => inner ℝ y (Y t ω)) P = 0) →
          ProbabilityTheory.IndepFun (fun ω s => X s ω) (fun ω t => Y t ω) P
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.Const.alter.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive x
-- Batteries.Data.Fin.Coding
Fin.decodeEmpty_encodeEmpty : ∀ (x : Empty), (Fin.encodeEmpty x).decodeEmpty = x
-- Mathlib.Order.Hom.BoundedLattice
/-- The type of bounded lattice homomorphisms from `α` to `β`.  -/
BoundedLatticeHom : (α : Type u_6) →
  (β : Type u_7) → [inst : Lattice α] → [inst_1 : Lattice β] → [BoundedOrder α] → [BoundedOrder β] → Type (max u_6 u_7)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.opCoproductIsoProduct'.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C}
  {c : CategoryTheory.Limits.Cofan Z} {f : CategoryTheory.Limits.Fan fun x => Opposite.op (Z x)}
  (hc : CategoryTheory.Limits.IsColimit c) (hf : CategoryTheory.Limits.IsLimit f),
  CategoryTheory.Limits.opCoproductIsoProduct' hc hf =
    (CategoryTheory.Limits.Cofan.IsColimit.op hc).conePointUniqueUpToIso hf
-- Init.Data.Array.Lemmas
/-- Variant of `all_eq` in terms of membership rather than an array index.  -/
Array.all_eq' : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, xs.all p = decide (∀ x ∈ xs, p x = true)
-- Mathlib.Data.List.Basic
List.succ_idxOf_lt_length_of_mem_dropLast : ∀ {α : Type u} [inst : BEq α] [LawfulBEq α] {l : List α} {a : α}, a ∈ l.dropLast → List.idxOf a l + 1 < l.length
-- Mathlib.RingTheory.Localization.FractionRing
/-- Given a commutative ring `A` with field of fractions `K`,
and an injective ring hom `g : A →+* L` where `L` is a field, we get a
field hom sending `z : K` to `g x * (g y)⁻¹`, where `(x, y) : A × (NonZeroDivisors A)` are
such that `z = f x * (f y)⁻¹`.  -/
IsFractionRing.lift : {A : Type u_4} →
  [inst : CommRing A] →
    {K : Type u_5} →
      [inst_1 : Field K] →
        {L : Type u_7} →
          [inst_2 : Field L] →
            [inst_3 : Algebra A K] → [IsFractionRing A K] → {g : A →+* L} → Function.Injective ⇑g → K →+* L
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.Ring.natCastFn? : Lean.Meta.Grind.Arith.CommRing.Ring → Option Lean.Expr
-- Mathlib.Order.WellFoundedSet
Set.WellFoundedOn.sdiff_singleton : ∀ {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] {s : Set α},
  s.WellFoundedOn r → ∀ (a : α), (s \ {a}).WellFoundedOn r
-- Mathlib.Order.Interval.Set.Basic
Set.Iio_one_eq_empty : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : One α] [IsBotOneClass α], Set.Iio 1 = ∅
-- Lean.Elab.Deriving.Util
Lean.Elab.Deriving.Header.mk : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder) →
  Array Lean.Name → Array Lean.Name → Lean.Term → Lean.Elab.Deriving.Header
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.norm_inv_eq : ∀ {α : Type u_1} [inst : DecidableEq α] {x : FreeGroup α}, x⁻¹.norm = x.norm
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.sub_self : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y : C}
  (a : X ⟶ Y), a - a = 0
-- Init.Data.UInt.Lemmas
UInt16.ofInt_mul : ∀ (x y : ℤ), UInt16.ofInt (x * y) = UInt16.ofInt x * UInt16.ofInt y
-- Init.WFComputable
Acc.ndrec.eq_1 : ∀ {α : Sort u2} {r : α → α → Prop} {C : α → Sort u1}
  (m : (x : α) → (∀ (y : α), r y x → Acc r y) → ((y : α) → r y x → C y) → C x) {a : α} (n : Acc r a),
  Acc.ndrec m n = Acc.rec m n
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get_eq_getD : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {a : α} {fallback : β a} {h : m.contains a = true}, m.get a h = m.getD a fallback
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.mem_left_iff_eq_zero_of_disjoint : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p p' : Submodule R M}, Disjoint p p' → ∀ {x : ↥p'}, ↑x ∈ p ↔ x = 0