mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonCreateFile.fromJson : Lean.Json → Except String Lean.Lsp.CreateFile
-- Mathlib.Analysis.Calculus.FDeriv.Prod
hasFDerivAtFilter_snd : ∀ {𝕜 : 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]
  {L : Filter ((E × F) × E × F)}, HasFDerivAtFilter Prod.snd (ContinuousLinearMap.snd 𝕜 E F) L
-- Mathlib.CategoryTheory.Action.Monoidal
Action.leftRegularTensorIso_hom_hom : ∀ (G : Type u) [inst : Group G] (X : Action (Type u) G),
  (Action.leftRegularTensorIso G X).hom.hom =
    { toFun := fun g => (g.1, (CategoryTheory.ConcreteCategory.hom (X.ρ g.1⁻¹)) g.2),
          invFun := fun g => (g.1, (CategoryTheory.ConcreteCategory.hom (X.ρ g.1)) g.2), left_inv := ⋯,
          right_inv := ⋯ }.toIso.hom
-- Mathlib.Topology.Order.WithTop
TopologicalSpace.instWithTopOfOrderTopology.eq_1 : ∀ {ι : Type u_1} [inst : Preorder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι],
  TopologicalSpace.instWithTopOfOrderTopology = Preorder.topology (WithTop ι)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
/-- Add instances `borel e : MeasurableSpace e` and `⟨rfl⟩ : BorelSpace e`.  -/
Mathlib.Tactic.Borelize.addBorelInstance : Lean.Expr → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.mk.injEq : ∀ {G : Type u_6} [inst : AddGroup G] (toZeroHom : ZeroHom G ℝ)
  (add_le_max' : ∀ (r s : G), toZeroHom.toFun (r + s) ≤ max (toZeroHom.toFun r) (toZeroHom.toFun s))
  (neg' : ∀ (r : G), toZeroHom.toFun (-r) = toZeroHom.toFun r) (toZeroHom_1 : ZeroHom G ℝ)
  (add_le_max'_1 : ∀ (r s : G), toZeroHom_1.toFun (r + s) ≤ max (toZeroHom_1.toFun r) (toZeroHom_1.toFun s))
  (neg'_1 : ∀ (r : G), toZeroHom_1.toFun (-r) = toZeroHom_1.toFun r),
  ({ toZeroHom := toZeroHom, add_le_max' := add_le_max', neg' := neg' } =
      { toZeroHom := toZeroHom_1, add_le_max' := add_le_max'_1, neg' := neg'_1 }) =
    (toZeroHom = toZeroHom_1)
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.single_source : ∀ {α : Type u_1} {β : Type u_2} (a : α) (b : β), (PartialEquiv.single a b).source = {a}
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.union : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {s t : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] [TopologicalSpace.PseudoMetrizableSpace ε],
  MeasureTheory.IntegrableOn f s μ → MeasureTheory.IntegrableOn f t μ → MeasureTheory.IntegrableOn f (s ∪ t) μ
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.inst : {M : Type u_1} → {N : Type u_2} → [inst : AddMonoid M] → [inst_1 : AddMonoid N] → AddMonoid (AddMonoid.Coprod M N)
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.comp_apply : ∀ {R : Type u} [inst : CommRing R] {A B C : CommHopfAlgCat R} (f : A ⟶ B) (g : B ⟶ C) (a : ↑A),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) a =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) a)
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.φ_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.kernelCokernelCompSequence.φ f g)
      (CategoryTheory.kernelCokernelCompSequence.π f g) =
    0
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Hom.comap_apply : ∀ {V : Type u_1} {W : Type u_2} (f : V → W) (G : SimpleGraph W) (a : V), (SimpleGraph.Hom.comap f G) a = f a
-- Lean.Widget.InteractiveDiagnostic
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.EmbedFmt.goal.inj : ∀ {ctx : Lean.Elab.ContextInfo} {lctx : Lean.LocalContext} {g : Lean.MVarId} {ctx_1 : Lean.Elab.ContextInfo}
  {lctx_1 : Lean.LocalContext} {g_1 : Lean.MVarId},
  Lean.Widget.EmbedFmt.goal✝ ctx lctx g = Lean.Widget.EmbedFmt.goal✝ ctx_1 lctx_1 g_1 →
    ctx = ctx_1 ∧ lctx = lctx_1 ∧ g = g_1
-- Mathlib.Topology.Connected.Clopen
/-- A set `s` is connected if and only if
for every cover by a finite collection of open sets that are pairwise disjoint on `s`,
it is contained in one of the members of the collection.  -/
isConnected_iff_sUnion_disjoint_open : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α},
  IsConnected s ↔
    ∀ (U : Finset (Set α)),
      (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
        (∀ u ∈ U, IsOpen u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
-- Mathlib.Analysis.Normed.MulAction
nndist_smul_le : ∀ {α : Type u_1} {β : Type u_2} [inst : SeminormedAddGroup α] [inst_1 : SeminormedAddGroup β]
  [inst_2 : SMulZeroClass α β] [IsBoundedSMul α β] (s : α) (x y : β), nndist (s • x) (s • y) ≤ ‖s‖₊ * nndist x y
-- Mathlib.Algebra.CharP.Frobenius
LinearMap.iterateFrobenius_def : ∀ (R : Type u_1) [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] (p : ℕ) [inst_2 : ExpChar R p]
  [inst_3 : ExpChar S p] [inst_4 : Algebra R S] (n : ℕ) (x : S), (LinearMap.iterateFrobenius R S p n) x = x ^ p ^ n
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.liftToInitialUnique_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) (hZ : CategoryTheory.Limits.IsInitial Z)
  (G : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (h : CategoryTheory.WithInitial.incl.comp G ≅ F)
  (hG : G.obj CategoryTheory.WithInitial.star ≅ Z) (X : CategoryTheory.WithInitial C),
  (CategoryTheory.WithInitial.liftToInitialUnique F hZ G h hG).inv.app X =
    (match X with
      | CategoryTheory.WithInitial.of x => h.app x
      | CategoryTheory.WithInitial.star => hG).inv
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.replicateRow_mul_replicateCol : ∀ {m : Type u_2} {α : Type v} {ι : Type u_6} [inst : Fintype m] [inst_1 : Mul α] [inst_2 : AddCommMonoid α]
  (v w : m → α), Matrix.replicateRow ι v * Matrix.replicateCol ι w = Matrix.of fun x x_1 => v ⬝ᵥ w
-- Mathlib.Analysis.Fourier.AddCircle
AddCircle.liftIoc.congr_simp : ∀ {𝕜 : Type u_1} {B : Type u_2} [inst : AddCommGroup 𝕜] (p : 𝕜) [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [hp : Fact (0 < p)] (a a_1 : 𝕜),
  a = a_1 →
    ∀ [inst_3 : Archimedean 𝕜] (f f_1 : 𝕜 → B),
      f = f_1 → ∀ (a_2 a_3 : AddCircle p), a_2 = a_3 → AddCircle.liftIoc p a f a_2 = AddCircle.liftIoc p a_1 f_1 a_3
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Cotrident.condition : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} (j₁ j₂ : J)
  (t : CategoryTheory.Limits.Cotrident f),
  CategoryTheory.CategoryStruct.comp (f j₁) t.π = CategoryTheory.CategoryStruct.comp (f j₂) t.π
-- Mathlib.Data.Rat.NatSqrt.Defs
/-- Approximate the square root of a natural number as a rational number, to within `1 / prec`.
 -/
Nat.ratSqrt : ℕ → ℕ → ℚ
-- Mathlib.Topology.Compactness.CompactSystem
/-- To prove that a set of sets is a compact system, it suffices to consider directed families of
sets.  -/
isCompactSystem_iff_nonempty_iInter_of_directed : ∀ {α : Type u_1} {S : Set (Set α)},
  IsPiSystem S →
    (IsCompactSystem S ↔
      ∀ (C : ℕ → Set α),
        Directed (fun x1 x2 => x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (C n).Nonempty) → (⋂ i, C i).Nonempty)
-- Init.Data.String.Lemmas.Splits
String.Pos.splits_cast_iff : ∀ {s₁ s₂ : String} {h : s₁ = s₂} {p : s₁.Pos} {t₁ t₂ : String}, (p.cast h).Splits t₁ t₂ ↔ p.Splits t₁ t₂
-- Mathlib.Algebra.Group.Basic
rightInverse_inv : ∀ (G : Type u_3) [inst : InvolutiveInv G], Function.RightInverse (fun a => a⁻¹) fun a => a⁻¹
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- The operator norm of a continuous multilinear map is the inf of all its bounds.  -/
ContinuousMultilinearMap.opNorm : {𝕜 : Type u} →
  {ι : Type v} →
    {E : ι → Type wE} →
      {G : Type wG} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
            [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] →
              [inst_3 : SeminormedAddCommGroup G] →
                [inst_4 : NormedSpace 𝕜 G] → [Fintype ι] → ContinuousMultilinearMap 𝕜 E G → ℝ
-- Plausible.Arbitrary
Plausible.Nat.Arbitrary : Plausible.Arbitrary ℕ
-- Mathlib.Data.Int.GCD
Nat.xgcd.eq_1 : ∀ (x y : ℕ), x.xgcd y = (x.xgcdAux 1 0 y 0 1).2
-- Mathlib.Data.Fin.Embedding
/-- `Fin.natAdd` as an `Embedding`, `natAddEmb n i` adds `n` to `i` "on the left".  -/
Fin.natAddEmb : (n : ℕ) → {m : ℕ} → Fin m ↪ Fin (n + m)
-- Mathlib.RingTheory.PolynomialLaw.Basic
/-- Extension of `PolynomialLaw.add_def`  -/
PolynomialLaw.toFun_add : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_3} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_4}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (f g : M →ₚₗ[R] N) {S : Type u_5} [inst_5 : CommSemiring S]
  [inst_6 : Algebra R S], PolynomialLaw.toFun S (f + g) = PolynomialLaw.toFun S f + PolynomialLaw.toFun S g
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.ofHasPushout_pt : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₂ Y₂ : C₂} (f₂ : X₂ ⟶ Y₂)
  [inst_3 : CategoryTheory.Limits.HasPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂)],
  (CategoryTheory.Functor.PushoutObjObj.ofHasPushout F f₁ f₂).pt =
    CategoryTheory.Limits.pushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂)
-- Mathlib.LinearAlgebra.Pi
LinearEquiv.piCongrRight_apply : ∀ {R : Type u} {ι : Type x} [inst : Semiring R] {φ : ι → Type u_1} {ψ : ι → Type u_2}
  [inst_1 : (i : ι) → AddCommMonoid (φ i)] [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : (i : ι) → AddCommMonoid (ψ i)]
  [inst_4 : (i : ι) → Module R (ψ i)] (e : (i : ι) → φ i ≃ₗ[R] ψ i) (f : (i : ι) → φ i) (i : ι),
  (LinearEquiv.piCongrRight e) f i = (e i) (f i)
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithTop.instInfSet.eq_1 : ∀ {α : Type u_1} [inst : LE α] [inst_1 : InfSet α],
  WithTop.instInfSet = { sInf := fun S => if S ⊆ {⊤} ∨ ¬BddBelow S then ⊤ else ↑(sInf ((fun a => ↑a) ⁻¹' S)) }
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.fromSingleMk_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ}
  (h : p + n = q),
  CochainComplex.HomComplex.Cochain.fromSingleMk (-f) h = -CochainComplex.HomComplex.Cochain.fromSingleMk f h
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoUniformly.sub : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3}
  {l : Filter ι} {f f' : ι → β → α} {g g' : β → α},
  TendstoUniformly f g l → TendstoUniformly f' g' l → TendstoUniformly (f - f') (g - g') l
-- Aesop.RuleTac.GoalDiff
/-- The old goal.  -/
Aesop.GoalDiff.oldGoal : Aesop.GoalDiff → Lean.MVarId
-- Mathlib.CategoryTheory.Retract
CategoryTheory.RetractArrow.retract_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : Y ⟶ X} {g : W ⟶ Z}
  (h : CategoryTheory.RetractArrow f g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right h.i) (CategoryTheory.Arrow.Hom.right h.r) =
    CategoryTheory.CategoryStruct.id X
-- Std.Http.Protocol.H1.Reader
/-- Unified body-reading state.
 -/
Std.Http.Protocol.H1.Reader.State.readBody : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Reader.BodyState → Std.Http.Protocol.H1.Reader.State dir
-- Mathlib.RingTheory.PowerSeries.Basic
/-- Split off the constant coefficient.  -/
PowerSeries.eq_X_mul_shift_add_const : ∀ {R : Type u_1} [inst : Semiring R] (φ : PowerSeries R),
  φ =
    (PowerSeries.X * PowerSeries.mk fun p => (PowerSeries.coeff (p + 1)) φ) +
      PowerSeries.C (PowerSeries.constantCoeff φ)
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.corootSpan_mem_invtSubmodule_coreflection : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [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 : ι),
  P.corootSpan R ∈ Module.End.invtSubmodule ↑(P.coreflection i)
-- Mathlib.Topology.UniformSpace.Basic
UniformContinuous.continuous : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  UniformContinuous f → Continuous f
-- Mathlib.Combinatorics.SimpleGraph.Density
SimpleGraph.interedges_disjoint_right : ∀ {α : Type u_4} (G : SimpleGraph α) [inst : DecidableRel G.Adj] {t₁ t₂ : Finset α} (s : Finset α),
  Disjoint t₁ t₂ → Disjoint (G.interedges s t₁) (G.interedges s t₂)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_
/-- The yoneda embedding of `CommGrp C` into presheaves of groups.  -/
CategoryTheory.yonedaCommGrpGrpObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        CategoryTheory.CommGrp C → CategoryTheory.Functor (CategoryTheory.Grp C)ᵒᵖ CommGrpCat
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasSumUniformly.summableUniformly : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α}
  [inst_1 : UniformSpace α], HasSumUniformly f g → SummableUniformly f
-- Init.Data.BitVec.Lemmas
BitVec.toNat_inj : ∀ {n : ℕ} {x y : BitVec n}, x.toNat = y.toNat ↔ x = y
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
CategoryTheory.Limits.zeroCoprodIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
  (CategoryTheory.Limits.zeroCoprodIso X).inv = CategoryTheory.Limits.coprod.inr
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.mem_smul_pointwise_iff_exists : ∀ {α : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : Monoid α] [inst_2 : MulDistribMulAction α M] (m : M) (a : α)
  (S : Submonoid M), m ∈ a • S ↔ ∃ s ∈ S, a • s = m
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.mem_congr : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x y : α} [Std.TransCmp cmp] {t : RBTree.RBSet α cmp},
  cmp x y = Ordering.eq → (x ∈ t ↔ y ∈ t)
-- Lean.Elab.InfoTree.Main
Lean.Elab.getInfoTrees : {m : Type → Type} → [Lean.Elab.MonadInfoTree m] → [Monad m] → m (Lean.PersistentArray Lean.Elab.InfoTree)
-- Mathlib.Analysis.Convex.Basic
convex_vadd : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {s : Set E} (a : E), Convex 𝕜 (a +ᵥ s) ↔ Convex 𝕜 s
-- Std.Internal.Do.WP.Lemmas
_private.Std.Internal.Do.WP.Lemmas.0.ExceptT.run_bind.match_1.eq_2 : ∀ {ε α : Type u_1} (motive : Except ε α → Sort u_2) (e : ε) (h_1 : (x : α) → motive (Except.ok x))
  (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.error e with
    | Except.ok x => h_1 x
    | Except.error e => h_2 e) =
    h_2 e
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.coe_toAddHom : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : M →ₛₗ[σ] M₃), ⇑f.toAddHom = ⇑f
-- Std.Http.Data.Status
/-- 101 Switching Protocols
 -/
Std.Http.Status.switchingProtocols : Std.Http.Status
-- Init.Data.SInt.Lemmas
Int16.toInt32_ofInt : ∀ {n : ℤ}, Int16.minValue.toInt ≤ n → n ≤ Int16.maxValue.toInt → (Int16.ofInt n).toInt32 = Int32.ofInt n
-- Mathlib.Data.ENNReal.Inv
ENNReal.mul_div_mul_comm : ∀ {a b c d : ENNReal}, c ≠ 0 ∨ d ≠ ⊤ → c ≠ ⊤ ∨ d ≠ 0 → a * b / (c * d) = a / c * (b / d)
-- Mathlib.RingTheory.Valuation.LocalSubring
IsLocalRing.exists_factor_valuationRing : ∀ {R : Type u_1} {K : Type u_3} [inst : CommRing R] [inst_1 : Field K] [IsLocalRing R] (f : R →+* K),
  ∃ A, ∃ (h : ∀ (x : R), f x ∈ A.toSubring), IsLocalHom (f.codRestrict A.toSubring h)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_mul_left₀ : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : Mul β] [MeasurableMul₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), AEMeasurable (f i) μ) → ∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.IndepFun (f i * f j) (f k) μ
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.const_one : ∀ {R A : Type u} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)),
  AlgebraicGeometry.StructureSheaf.const 1 1 U ⋯ = 1
-- Init.Data.SInt.Bitwise
Int64.neg_one_shiftLeft_or_shiftLeft : ∀ {a b : Int64}, (-1) <<< b ||| a <<< b = (-1) <<< b
-- Mathlib.Algebra.Group.Defs
/-- Any `CommMagma G` that satisfies `IsLeftCancelMul G` also satisfies `IsRightCancelMul G`.  -/
CommMagma.IsLeftCancelMul.toIsRightCancelMul : ∀ (G : Type u) [inst : CommMagma G] [IsLeftCancelMul G], IsRightCancelMul G
-- Mathlib.GroupTheory.Congruence.Opposite
AddCon.orderIsoOp_apply : ∀ {M : Type u_1} [inst : Add M] (c : AddCon M), AddCon.orderIsoOp c = c.op
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.inducedOuterMeasure_eq' : ∀ {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0}
  (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)),
  (∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯) →
    (∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) →
      ∀ {s : Set α} (hs : P s), (MeasureTheory.inducedOuterMeasure m P0 m0) s = m s hs
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
CategoryTheory.Limits.Types.Pushout.inl_eq_inr_iff : ∀ {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) [CategoryTheory.Mono f] (x₁ : X₁) (x₂ : X₂),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.Pushout.inl f g)) x₁ =
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.Pushout.inr f g)) x₂ ↔
    ∃ s, (CategoryTheory.ConcreteCategory.hom f) s = x₁ ∧ (CategoryTheory.ConcreteCategory.hom g) s = x₂
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
Lean.Elab.ConfigEval.instBEqEvalConfigItemHandlerKind : BEq Lean.Elab.ConfigEval.EvalConfigItemHandlerKind
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.extend_top : ∀ {α : Type u_3} {P : α → Prop}, (MeasureTheory.extend fun x x_1 => ⊤) = ⊤
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.arrayLit.sizeOf_spec : ∀ (type : Lean.Expr) (xs : List Lean.Meta.Match.Pattern),
  sizeOf (Lean.Meta.Match.Pattern.arrayLit type xs) = 1 + sizeOf type + sizeOf xs
-- Mathlib.Analysis.Convex.Body
ConvexBody.instAddMonoid : {V : Type u_1} →
  [inst : TopologicalSpace V] →
    [inst_1 : AddCommGroup V] → [inst_2 : Module ℝ V] → [ContinuousAdd V] → AddMonoid (ConvexBody V)
-- Mathlib.Algebra.MonoidAlgebra.Division
AddMonoidAlgebra.mul_of'_modOf : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] (x : AddMonoidAlgebra k G) (g : G),
  (x * AddMonoidAlgebra.of' k G g).modOf g = 0
-- Init.Data.List.Lemmas
List.flatMap_def : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β}, List.flatMap f l = (List.map f l).flatten
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
DifferentiableOn.ccosh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {s : Set E},
  DifferentiableOn ℂ f s → DifferentiableOn ℂ (fun x => Complex.cosh (f x)) s
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- **Alias** of `CategoryTheory.Mod.forget`.

---

The forgetful functor from module objects to the ambient category.  -/
CategoryTheory.Mod_.forget : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            (A : C) → [inst_4 : CategoryTheory.MonObj A] → CategoryTheory.Functor (CategoryTheory.Mod D A) D
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.cartanEquivDual.congr_simp : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] (H : LieSubalgebra K L) [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L], LieAlgebra.IsKilling.cartanEquivDual H = LieAlgebra.IsKilling.cartanEquivDual H
-- Lean.Parser.Command
Lean.Parser.Command.deriving.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Complex.Basic
Complex.ofReal_tsum : ∀ {α : Type u_1} {L : SummationFilter α} (f : α → ℝ), ↑(∑'[L] (a : α), f a) = ∑'[L] (a : α), ↑(f a)
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn'_rcc : ∀ {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] [inst_4 : LE α]
  [inst_5 : DecidableLE α] [inst_6 : Std.PRange.UpwardEnumerable α] [inst_7 : Std.Rxc.IsAlwaysFinite α]
  [inst_8 : Std.PRange.LawfulUpwardEnumerable α] [inst_9 : Std.PRange.LawfulUpwardEnumerableLE α] {xs : Std.Rcc α}
  {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Std.Internal.Do.Invariant xs.toList β Pred)
  {epost : EPred},
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f cur ⋯ b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'
        | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b';
        epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init ⦄ forIn' xs init f ⦃ fun b =>
      inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b; epost ⦄
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.HasProjectiveResolutions.congr_simp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C],
  CategoryTheory.HasProjectiveResolutions C = CategoryTheory.HasProjectiveResolutions C
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreeOf_zero : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (n : σ), MvPolynomial.degreeOf n 0 = 0
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.head?_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Min α] [inst_2 : LE α] [Std.LawfulOrderCmp cmp] [Std.LawfulOrderMin α] [Std.LawfulOrderLeftLeaningMin α]
  [Std.LawfulEqCmp cmp], t.keys.head? = t.minKey?
-- Mathlib.Analysis.Calculus.Deriv.Add
HasStrictDerivAt.sub : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {f' g' : F} {x : 𝕜},
  HasStrictDerivAt f f' x → HasStrictDerivAt g g' x → HasStrictDerivAt (f - g) (f' - g') x
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_C_mul_X_le : ∀ {R : Type u} [inst : Semiring R] (a : R), (Polynomial.C a * Polynomial.X).degree ≤ 1
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedProcess_const : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {τ : Ω → WithTop ι} [inst_1 : LinearOrder ι]
  {u₀ : Ω → β}, MeasureTheory.stoppedProcess (fun x => u₀) τ = fun x => u₀
-- Init.Data.Nat.Lcm
Nat.lcm_mul_right_left_eq_mul_of_lcm_eq_mul : ∀ {n m k : ℕ}, n.lcm m = n * m → (n * k).lcm m = n * k.lcm m
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Associates.le_singleton_iff : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A] (x : A) (n : ℕ) (I : Ideal A),
  Associates.mk I ^ n ≤ Associates.mk (Ideal.span {x}) ↔ x ∈ I ^ n