mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Process.Filtration
/-- Given an integrable function `g`, the conditional expectations of `g` with respect to a
filtration is uniformly integrable.  -/
MeasureTheory.Integrable.uniformIntegrable_condExp_filtration : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure μ] {f : MeasureTheory.Filtration ι m} {g : Ω → ℝ},
  MeasureTheory.Integrable g μ → MeasureTheory.UniformIntegrable (fun i => μ[g | ↑f i]) 1 μ
-- Init.Control.Lawful.Instances
ReaderT.run_control : ∀ {m : Type u → Type u_1} {ρ α : Type u} [inst : Monad m] [LawfulMonad m]
  (f : ({β : Type u} → ReaderT ρ m β → m (stM m (ReaderT ρ m) β)) → m (stM m (ReaderT ρ m) α)) (ctx : ρ),
  (control f).run ctx = f fun {β} x => x.run ctx
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
finsuppTensorFinsupp_symm_single : ∀ (R : Type u_1) (S : Type u_2) (M : Type u_3) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  [inst_5 : Semiring S] [inst_6 : Algebra R S] [inst_7 : Module S M] [inst_8 : IsScalarTower R S M] (i : ι × κ) (m : M)
  (n : N), ((finsuppTensorFinsupp R S M N ι κ).symm fun₀ | i => m ⊗ₜ[R] n) = (fun₀ | i.1 => m) ⊗ₜ[R] fun₀ | i.2 => n
-- Mathlib.AlgebraicTopology.SingularHomology.HomologyZero
TopCat.singularHomology₀Iso_sigma_desc_id_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.CategoryWithHomology C] (X : TopCat) (R : C) {Z : C}
  (h : R ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.singularHomology₀Iso R).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.desc fun x => CategoryTheory.CategoryStruct.id R)
        h) =
    CategoryTheory.CategoryStruct.comp (X.singularHomology₀ε R) h
-- Mathlib.CategoryTheory.Bicategory.Opposites
CategoryTheory.Iso.unop2_op2 : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : Bᵒᵖ} {f g : a ⟶ b} (η : f ≅ g), η.unop2.op2 = η
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
/-- The inverse trivialization of the tangent bundle at a point is the manifold derivative of the
inverse of the extended chart.
Use with care as this abuses the defeq `TangentSpace 𝓘(𝕜, E) y = E` for `y : E`.  -/
TangentBundle.symmL_trivializationAt : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] {x₀ x : M},
  x ∈ (chartAt H x₀).source →
    Bundle.Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) x₀) x =
      mfderiv[Set.range ↑I] ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.lineMap_apply : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] (p₀ p₁ : P1) (c : k), (AffineMap.lineMap p₀ p₁) c = c • (p₁ -ᵥ p₀) +ᵥ p₀
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {a b : α} (hab : cmp a b = Ordering.eq) {h' : a ∈ t},
  Std.ExtDTreeMap.Const.get t a h' = Std.ExtDTreeMap.Const.get t b ⋯
-- Mathlib.RingTheory.Localization.FractionRing
/-- A ring automorphism of a ring induces an ring automorphism of its fraction field.

This is a bundled version of `ringEquivOfRingEquiv`.  -/
IsFractionRing.ringEquivOfRingEquivHom : (A : Type u_8) →
  (K : Type u_9) →
    [inst : CommRing A] → [inst_1 : CommRing K] → [inst_2 : Algebra A K] → [IsFractionRing A K] → (A ≃+* A) →* K ≃+* K
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.truncate_truncate : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] {n₁ n₂ n₃ : ℕ} (h1 : n₁ ≤ n₂) (h2 : n₂ ≤ n₃)
  (x : TruncatedWittVector p n₃ R),
  (TruncatedWittVector.truncate h1) ((TruncatedWittVector.truncate h2) x) = (TruncatedWittVector.truncate ⋯) x
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.of.sizeOf_spec : ∀ {C : Type u} [inst : SizeOf C] (a : C), sizeOf (CategoryTheory.WithTerminal.of a) = 1 + sizeOf a
-- Mathlib.Algebra.Order.Floor.Extended
ENat.floor_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], ⌊OfNat.ofNat n⌋ₑ = OfNat.ofNat n
-- Init.Data.Option.Basic
Option.instMin : {α : Type u_1} → [Min α] → Min (Option α)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.mk.injEq : ∀ (ω₁ ω₂ : ℂ) (indep : LinearIndependent ℝ ![ω₁, ω₂]) (ω₁_1 ω₂_1 : ℂ) (indep_1 : LinearIndependent ℝ ![ω₁_1, ω₂_1]),
  ({ ω₁ := ω₁, ω₂ := ω₂, indep := indep } = { ω₁ := ω₁_1, ω₂ := ω₂_1, indep := indep_1 }) = (ω₁ = ω₁_1 ∧ ω₂ = ω₂_1)
-- Lean.LibrarySuggestions.SineQuaNon
_private.Lean.LibrarySuggestions.SineQuaNon.0.Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_3 : Lean.Environment → Lean.OLeanEntries (Array (Lean.NameMap (List (Lean.Name × Float))))
-- Mathlib.Algebra.Lie.SkewAdjoint
/-- An invertible matrix `P` gives a Lie algebra equivalence between those endomorphisms that are
skew-adjoint with respect to a square matrix `J` and those with respect to `PᵀJP`.  -/
skewAdjointMatricesLieSubalgebraEquiv : {R : Type u} →
  {n : Type w} →
    [inst : CommRing R] →
      [inst_1 : Fintype n] →
        (J : Matrix n n R) →
          [inst_2 : DecidableEq n] →
            (P : Matrix n n R) →
              Invertible P →
                ↥(skewAdjointMatricesLieSubalgebra J) ≃ₗ⁅R⁆ ↥(skewAdjointMatricesLieSubalgebra (P.transpose * J * P))
-- Mathlib.Topology.Constructions
IsDiscrete.to_subtype : ∀ {X : Type u_5} [inst : TopologicalSpace X] {s : Set X}, IsDiscrete s → DiscreteTopology ↑s
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.addMonoidWithOne : {α : Type u} → [AddMonoidWithOne α] → AddMonoidWithOne (WithTop α)
-- Mathlib.Order.Preorder.Finsupp
Finsupp.sup_apply : ∀ {ι : Type u_1} {M : Type u_2} [inst : Zero M] [inst_1 : SemilatticeSup M] (f g : ι →₀ M) (i : ι),
  (f ⊔ g) i = f i ⊔ g i
-- Init.Data.String.Basic
ByteArray.isSome_utf8Decode?_eq_validateUTF8 : ∀ {b : ByteArray}, b.utf8Decode?.isSome = b.validateUTF8
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.toAlgHom_ofAlgHom : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : f.comp g = AlgHom.id R A₂)
  (h₂ : g.comp f = AlgHom.id R A₁), ↑(AlgEquiv.ofAlgHom f g h₁ h₂) = f
-- Batteries.Lean.EStateM
EStateM.run_map : ∀ {α β ε σ : Type u_1} (f : α → β) (x : EStateM ε σ α) (s : σ), (f <$> x).run s = EStateM.Result.map f (x.run s)
-- Lean.Meta.Tactic.Grind.Types
/-- Given a new disequality `lhs ≠ rhs`, propagates it to relevant theories.
 -/
Lean.Meta.Grind.Solvers.propagateDiseqs : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.LinearAlgebra.Matrix.Defs
/-- The top `u × n` part of a `(u+d) × n` matrix.  -/
Matrix.subUp : {α : Type v} → {d u n : ℕ} → Matrix (Fin (u + d)) (Fin n) α → Matrix (Fin u) (Fin n) α
-- Mathlib.Tactic.Ring.Common
/-- `ExBase BaseType sα e` stores the structure of a normalized expression `e`, which appears
as the base of an exponent expression `e^n`. The `sum` constructor is only used when the exponent
`n` is not a constant.  -/
Mathlib.Tactic.Ring.Common.ExBase : {u : Lean.Level} → {α : Q(Type u)} → (Q(«$α») → Type) → Q(CommSemiring «$α») → Q(«$α») → Type
-- Init.Data.UInt.Lemmas
UInt64.toUInt16_ofNat' : ∀ (n : ℕ), (UInt64.ofNat n).toUInt16 = UInt16.ofNat n
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.isTopologicalBasis_basic_opens : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜], TopologicalSpace.IsTopologicalBasis (Set.range fun r => ↑(ProjectiveSpectrum.basicOpen 𝒜 r))
-- Mathlib.Order.Bounds.Basic
bbdAbove_range_left_of_sup : ∀ {ι : Sort u_4} {α : Type u_5} [inst : SemilatticeSup α] {f g : ι → α},
  BddAbove (Set.range fun x => f x ⊔ g x) → BddAbove (Set.range f)
-- Mathlib.Geometry.Manifold.IntegralCurve.Basic
IsMIntegralCurveAt.continuousAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x} {t₀ : ℝ}, IsMIntegralCurveAt γ v t₀ → ContinuousAt γ t₀
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.postEquiv_counitIso : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : T) (F : T ≌ D),
  (CategoryTheory.Under.postEquiv X F).counitIso =
    CategoryTheory.NatIso.ofComponents (fun A => CategoryTheory.Under.isoMk (F.counitIso.app A.right) ⋯) ⋯
-- Lean.Elab.DeclModifiers
Lean.Elab.Modifiers.recKind : Lean.Elab.Modifiers → Lean.Elab.RecKind
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.glue!.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) (sz' : ℕ) (k' : α) (v' : β k')
  (l'' r'' : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (r : Std.DTreeMap.Internal.Impl α β) →
      (sz' : ℕ) →
        (k' : α) →
          (v' : β k') →
            (l'' r'' : Std.DTreeMap.Internal.Impl α β) →
              r = Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'' →
                motive (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'')),
  (match Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'' with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | r@h:(Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'') => h_2 r sz' k' v' l'' r'' h) =
    h_2 (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'') sz' k' v' l'' r'' ⋯
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
/-- The homotopy category of bounded below cochain complexes.  -/
HomotopyCategory.Plus : (C : Type u_1) → [inst : CategoryTheory.Category.{v_1, u_1} C] → [CategoryTheory.Preadditive C] → Type (max u_1 v_1)
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.re_natCast : ∀ {R : Type u_1} {a b : R} [inst : AddCommMonoidWithOne R] (n : ℕ), (↑n).re = ↑n
-- Mathlib.Algebra.Algebra.Subalgebra.Prod
/-- The product of two subalgebras is a subalgebra.  -/
Subalgebra.prod : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Semiring B] → [inst_4 : Algebra R B] → Subalgebra R A → Subalgebra R B → Subalgebra R (A × B)
-- Mathlib.Algebra.Group.Action.Defs
IsCancelVAdd.eq_zero_of_vadd : ∀ {G : Type u_11} {P : Type u_12} [inst : AddMonoid G] [inst_1 : AddAction G P] [IsCancelVAdd G P] {g : G} {x : P},
  g +ᵥ x = x → g = 0
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonColorInformation.fromJson : Lean.Json → Except String Lean.Lsp.ColorInformation
-- Mathlib.Algebra.Order.Group.Basic
zpow_le_zpow_iff_left : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : LinearOrder α] [IsOrderedMonoid α] {n : ℤ} {a b : α},
  0 < n → (a ^ n ≤ b ^ n ↔ a ≤ b)
-- Mathlib.RingTheory.Finiteness.Descent
Ideal.FG.of_FG_map_of_faithfullyFlat : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Module.FaithfullyFlat R S] {I : Ideal R}, (Ideal.map (algebraMap R S) I).FG → I.FG
-- Mathlib.Data.Nat.Choose.Central
/-- The central binomial coefficient is the largest binomial coefficient.
 -/
Nat.choose_le_centralBinom : ∀ (r n : ℕ), (2 * n).choose r ≤ n.centralBinom
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.instCountableAB4OfAB4OfSize : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [CategoryTheory.AB4OfSize.{0, v, u} C], CategoryTheory.CountableAB4 C
-- Init.Data.BitVec.Bitblast
BitVec.ushiftRightRec.eq_2 : ∀ {w₁ w₂ : ℕ} (x : BitVec w₁) (y : BitVec w₂) (s_1 : ℕ),
  x.ushiftRightRec y s_1.succ = x.ushiftRightRec y s_1 >>> (y &&& BitVec.twoPow w₂ s_1.succ)
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.chainBotCoeff_of_eq_zsmul_add : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_6 : H.IsCartanSubalgebra]
  [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L),
  α.IsNonZero →
    ∀ (β' : LieModule.Weight K (↥H) L) (n : ℤ),
      ⇑β' = n • ⇑α + ⇑β → ↑(LieModule.chainBotCoeff (⇑α) β') = ↑(LieModule.chainBotCoeff (⇑α) β) + n
-- Std.Tactic.BVDecide.LRAT.Actions
Std.Tactic.BVDecide.LRAT.Action.addEmpty.sizeOf_spec : ∀ {β : Type u} {α : Type v} [inst : SizeOf β] [inst_1 : SizeOf α] (id : ℕ) (rupHints : Array ℕ),
  sizeOf (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints) = 1 + sizeOf id + sizeOf rupHints
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Set.mem_nsmul_iff_sum : ∀ {α : Type u_2} [inst : AddCommMonoid α] {n : ℕ} {s : Set α} {a : α},
  a ∈ n • s ↔ ∃ f, (∀ (i : Fin n), f i ∈ s) ∧ ∑ i, f i = a
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- **Alias** of `IsOpen.locallyPathConnectedSpace`. -/
IsOpen.locPathConnectedSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyPathConnectedSpace X] {U : Set X},
  IsOpen U → LocallyPathConnectedSpace ↑U
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.coe_eq_zero_iff : ∀ {R : Type u} [inst : NonAssocRing R] (s : Subring R) {x : ↥s}, ↑x = 0 ↔ x = 0
-- Mathlib.Algebra.Order.Antidiag.Tendsto
Finset.HasAntidiagonal.tendsto_sup'_antidiagonal_cofinite : ∀ {M : Type u_1} {R : Type u_2} [inst : AddMonoid M] [inst_1 : Finset.HasAntidiagonal M] {f : M × M → R}
  [inst_2 : LinearOrder R] {F : Filter R},
  Filter.Tendsto f Filter.cofinite F →
    Filter.Tendsto (fun a => (Finset.HasAntidiagonal.antidiagonal a).sup' ⋯ f) Filter.cofinite F
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.mkRat_nonpos_iff : ∀ (a : ℤ) {b : ℕ}, b ≠ 0 → (mkRat a b ≤ 0 ↔ a ≤ 0)
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- An additive monoid object as an additive module over itself.  -/
CategoryTheory.AddMod.regular : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (A : C) → [inst_2 : CategoryTheory.AddMonObj A] → CategoryTheory.AddMod C A
-- Mathlib.Probability.Distributions.Gamma
/-- The pdf of the gamma distribution depending on its scale and rate  -/
ProbabilityTheory.gammaPDFReal : ℝ → ℝ → ℝ → ℝ
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.mk.sizeOf_spec : ∀ {X : Type u_7} {Y : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : SizeOf X]
  [inst_3 : SizeOf Y] (toPartialEquiv : PartialEquiv X Y)
  (continuousOn_toFun : ContinuousOn (↑toPartialEquiv) toPartialEquiv.source)
  (continuousOn_invFun : ContinuousOn toPartialEquiv.invFun toPartialEquiv.target),
  sizeOf
      { toPartialEquiv := toPartialEquiv, continuousOn_toFun := continuousOn_toFun,
        continuousOn_invFun := continuousOn_invFun } =
    1 + sizeOf toPartialEquiv
-- Mathlib.Computability.TuringMachine.Config
/-- `nil` is the constant nil function: `nil v = []`.  -/
Turing.ToPartrec.Code.nil : Turing.ToPartrec.Code
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.BallPackage.mk.sizeOf_spec : ∀ {β : Type u_1} {α : Type u_2} [inst : SizeOf β] [inst_1 : SizeOf α] (c : β → α) (r : β → ℝ)
  (rpos : ∀ (b : β), 0 < r b) (r_bound : ℝ) (r_le : ∀ (b : β), r b ≤ r_bound),
  sizeOf { c := c, r := r, rpos := rpos, r_bound := r_bound, r_le := r_le } = 1 + sizeOf r_bound
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.succ_mem_succ_succ_iff : ∀ {α : Type u} [inst : LT α] [DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LinearlyUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.PRange.InfinitelyUpwardEnumerable α] [Std.Rxo.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α]
  {lo hi a : α}, (Std.PRange.succ a ∈ (Std.PRange.succ lo)<...Std.PRange.succ hi) ↔ a ∈ lo<...hi
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.map_lowerCentralSeries_eq : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] (k : ℕ) {M₂ : Type w₁}
  [inst_6 : AddCommGroup M₂] [inst_7 : Module R M₂] [inst_8 : LieRingModule L M₂] [LieModule R L M₂] [LieModule R L M]
  {f : M →ₗ⁅R,L⁆ M₂},
  Function.Surjective ⇑f →
    LieSubmodule.map f (LieModule.lowerCentralSeries R L M k) = LieModule.lowerCentralSeries R L M₂ k
-- Mathlib.Computability.Language
Language.one_def : ∀ {α : Type u_1}, 1 = {[]}
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.NormalizePattern.PatternArgKind.isSupport : Lean.Meta.Grind.NormalizePattern.PatternArgKind → Bool
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.OrdSet.mk.inj : ∀ {α : Type} {inst : Hashable α} {inst_1 : BEq α} {elems : Array α} {set : Std.HashSet α} {elems_1 : Array α}
  {set_1 : Std.HashSet α},
  { elems := elems, set := set } = { elems := elems_1, set := set_1 } → elems = elems_1 ∧ set = set_1
-- Mathlib.Tactic.Algebraize
/-- Configuration for `algebraize`.  -/
Mathlib.Tactic.Algebraize.Config : Type
-- Mathlib.Data.Sym.Sym2
_private.Mathlib.Data.Sym.Sym2.0.Sym2.fromVector : {α : Type u_1} → List.Vector α 2 → α × α
-- Mathlib.CategoryTheory.Abelian.Preradical.Basic
CategoryTheory.Abelian.Preradical.IsIdempotent.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {Φ : CategoryTheory.Abelian.Preradical C},
  CategoryTheory.IsIso (Φ.r.whiskerLeft Φ.ι) → Φ.IsIdempotent
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Module.rank_of_bijective_toSpanSingleton : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {x : M}, Function.Bijective ⇑(LinearMap.toSpanSingleton R M x) → Module.rank R M = 1
-- Mathlib.RingTheory.Algebraic.Basic
Subalgebra.isAlgebraic_iff_isAlgebraic_val : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {S : Subalgebra R A} {x : ↥S},
  IsAlgebraic R x ↔ IsAlgebraic R ↑x
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.instBot.eq_1 : ∀ {α : Type u_1} [inst : LE α], UpperSet.instBot = { bot := { carrier := Set.univ, upper' := ⋯ } }
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.instZero : {R : Type u} →
  {ι : Type v} →
    {M₁ : ι → Type w₁} →
      {M₂ : Type w₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] →
                    [inst_6 : TopologicalSpace M₂] → Zero (ContinuousMultilinearMap R M₁ M₂)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.single_zero_mul_eq_smul : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : Semiring R] {r : R} {x : HahnSeries Γ R}, (HahnSeries.single 0) r * x = r • x
-- Mathlib.Algebra.Order.Rearrangement
/-- **Equality case of the Rearrangement Inequality**: Pointwise scalar multiplication of `f` and
`g`, which antivary together, is unchanged by a permutation if and only if `f` and `g ∘ σ` antivary
together. Stated by permuting the entries of `g`.  -/
Antivary.sum_smul_comp_perm_eq_sum_smul_iff : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [ExistsAddOfLE α] [inst_4 : AddCommMonoid β] [inst_5 : LinearOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module α β] [PosSMulStrictMono α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [inst_9 : Fintype ι],
  Antivary f g → (∑ i, f i • g (σ i) = ∑ i, f i • g i ↔ Antivary f (g ∘ ⇑σ))
-- Lean.Parser.Basic
Lean.Parser.andthenInfo : Lean.Parser.ParserInfo → Lean.Parser.ParserInfo → Lean.Parser.ParserInfo
-- Mathlib.Tactic.FailIfNoProgress
_private.Mathlib.Tactic.FailIfNoProgress.0.Mathlib.Tactic.lctxIsDefEq.match_1.eq_5 : ∀ (motive : List (Option Lean.LocalDecl) → List (Option Lean.LocalDecl) → Sort u_1)
  (x x_1 : List (Option Lean.LocalDecl)) (h_1 : (l₁ l₂ : List (Option Lean.LocalDecl)) → motive (none :: l₁) l₂)
  (h_2 : (l₁ l₂ : List (Option Lean.LocalDecl)) → motive l₁ (none :: l₂))
  (h_3 :
    (d₁ : Lean.LocalDecl) →
      (l₁ : List (Option Lean.LocalDecl)) →
        (d₂ : Lean.LocalDecl) → (l₂ : List (Option Lean.LocalDecl)) → motive (some d₁ :: l₁) (some d₂ :: l₂))
  (h_4 : Unit → motive [] []) (h_5 : (x x_2 : List (Option Lean.LocalDecl)) → motive x x_2),
  (∀ (l₁ : List (Option Lean.LocalDecl)), x = none :: l₁ → False) →
    (∀ (l₂ : List (Option Lean.LocalDecl)), x_1 = none :: l₂ → False) →
      (∀ (d₁ : Lean.LocalDecl) (l₁ : List (Option Lean.LocalDecl)) (d₂ : Lean.LocalDecl)
          (l₂ : List (Option Lean.LocalDecl)), x = some d₁ :: l₁ → x_1 = some d₂ :: l₂ → False) →
        (x = [] → x_1 = [] → False) →
          (match x, x_1 with
            | none :: l₁, l₂ => h_1 l₁ l₂
            | l₁, none :: l₂ => h_2 l₁ l₂
            | some d₁ :: l₁, some d₂ :: l₂ => h_3 d₁ l₁ d₂ l₂
            | [], [] => h_4 ()
            | x, x_6 => h_5 x x_6) =
            h_5 x x_1
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Internal implementation detail of the iterator library.  -/
Std.IterM.Total.instForIn' : {m : Type w → Type w'} →
  {n : Type w → Type w''} →
    {α β : Type w} →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m n] →
          [MonadLiftT m n] →
            [Monad n] →
              [Std.Iterators.Finite α m] →
                ForIn' n (Std.IterM.Total m β) β { mem := fun it out => it.it.IsPlausibleIndirectOutput out }
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.zero_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData),
  (CategoryTheory.ShortComplex.HomologyMapData.zero h₁ h₂).left =
    CategoryTheory.ShortComplex.LeftHomologyMapData.zero h₁.left h₂.left
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.exists_mem : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι), ∃ x, x ∈ I
-- Mathlib.Order.Category.BddLat
_private.Mathlib.Order.Category.BddLat.0.BddLat.Hom.mk.sizeOf_spec : ∀ {X Y : BddLat} (hom' : BoundedLatticeHom ↑X.toLat ↑Y.toLat), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.Algebra.Homology.Embedding.TruncLE
HomologicalComplex.truncLE'XIsoCycles.eq_1 : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncLE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  {i : ι} {i' : ι'} (hi' : e.f i = i') (hi : e.BoundaryLE i),
  K.truncLE'XIsoCycles e hi' hi = (K.op.truncGE'XIsoOpcycles e.op hi' ⋯).unop.symm ≪≫ (K.opcyclesOpIso i').unop.symm
-- Mathlib.Order.Heyting.Boundary
Coheyting.boundary_le_hnot : ∀ {α : Type u_1} [inst : CoheytingAlgebra α] {a : α}, Coheyting.boundary a ≤ ￢a
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- The map on value groups-with-zero associated to the structure morphism of an algebra.  -/
ValuativeExtension.mapValueGroupWithZero : (A : Type u_1) →
  (B : Type u_2) →
    [inst : CommRing A] →
      [inst_1 : Ring B] →
        [inst_2 : ValuativeRel A] →
          [inst_3 : ValuativeRel B] →
            [inst_4 : Algebra A B] →
              [ValuativeExtension A B] → ValuativeRel.ValueGroupWithZero A →*₀ ValuativeRel.ValueGroupWithZero B