mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Sym.AlphaShareCommon
/-- Similar to `shareCommon`, but handles alpha-equivalence.

`cache` may contain the results of a previous run that failed with a check violation
(see `AlphaShareCommonM`); seeding the retry with it avoids revisiting the subterms
that were processed before the failure.
 -/
Lean.Meta.Sym.shareCommonAlpha : Lean.Expr → optParam Lean.Meta.Sym.AlphaShareCommon.Cache ∅ → Lean.Meta.Sym.AlphaShareCommonM Lean.Expr
-- Lean.Meta.Tactic.Grind.MatchDiscrOnly
/-- Adds `reduceSimpMatchDiscrsOnly` to `s`  -/
Lean.Meta.Grind.addSimpMatchDiscrsOnly : Lean.Meta.Simprocs → Lean.CoreM Lean.Meta.Simprocs
-- Mathlib.Analysis.SumOverResidueClass
/-- If `f : ℕ → ℝ` is decreasing and has a negative term, then `f` restricted to a residue
class is not summable.  -/
not_summable_indicator_mod_of_antitone_of_neg : ∀ {m : ℕ} [hm : NeZero m] {f : ℕ → ℝ},
  Antitone f → ∀ {n : ℕ}, f n < 0 → ∀ (k : ZMod m), ¬Summable ({n | ↑n = k}.indicator f)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mkPrecomp_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {Y Y' Y'' : C} {S : CategoryTheory.Functor C D} (f : S.obj Y ⟶ T) (g : Y' ⟶ Y) (g' : Y'' ⟶ Y'),
  CategoryTheory.CostructuredArrow.mkPrecomp f (CategoryTheory.CategoryStruct.comp g' g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.CostructuredArrow.mkPrecomp (CategoryTheory.CategoryStruct.comp (S.map g) f) g')
        (CategoryTheory.CostructuredArrow.mkPrecomp f g))
-- Mathlib.Data.QPF.Multivariate.Constructions.Comp
MvQPF.Comp.map_mk : ∀ {n m : ℕ} {F : TypeVec.{u} n → Type u_1} {G : Fin2 n → TypeVec.{u} m → Type u} {α β : TypeVec.{u} m} (f : α.Arrow β)
  [inst : MvFunctor F] [inst_1 : (i : Fin2 n) → MvFunctor (G i)] (x : F fun i => G i α),
  MvFunctor.map f (MvQPF.Comp.mk x) = MvQPF.Comp.mk (MvFunctor.map (fun i x => MvFunctor.map f x) x)
-- Mathlib.GroupTheory.Coset.Basic
AddSubgroup.quotientEquivProdOfLE'.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α] {s t : AddSubgroup α} (h_le : s ≤ t) (f : α ⧸ t → α)
  (hf : Function.RightInverse f QuotientAddGroup.mk),
  AddSubgroup.quotientEquivProdOfLE' h_le f hf =
    { toFun := fun a => (Quotient.map' id ⋯ a, Quotient.map' (fun g => ⟨-f (Quotient.mk'' g) + g, ⋯⟩) ⋯ a),
      invFun := fun a => Quotient.map' (fun b => f a.1 + ↑b) ⋯ a.2, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.univ_mem_measurableCylinders : ∀ {ι : Type u_2} (α : ι → Type u_1) [inst : (i : ι) → MeasurableSpace (α i)],
  Set.univ ∈ MeasureTheory.measurableCylinders α
-- Mathlib.Order.Defs.PartialOrder
instTransGTGE : {α : Type u_1} → [inst : Preorder α] → Trans GT.gt GE.ge GT.gt
-- Mathlib.Order.Monotone.MonovaryOrder
/-- **Alias** of the forward direction of `antivary_iff_exists_antitone_monotone`. -/
Antivary.exists_antitone_monotone : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : ι → α} {g : ι → β},
  Antivary f g → ∃ x, Antitone f ∧ Monotone g
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
/-- The 2-morphism in `C` underlying the 2-morphism in `InducedBicategory C F`.  -/
CategoryTheory.Bicategory.InducedBicategory.Hom₂.hom : {B : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Bicategory C] →
      {F : B → C} →
        {X Y : CategoryTheory.Bicategory.InducedBicategory C F} →
          {f g : X ⟶ Y} → CategoryTheory.Bicategory.InducedBicategory.Hom₂ f g → (f.hom ⟶ g.hom)
-- Mathlib.Geometry.Convex.ConvexSpace.Module
Convexity.instConvexSpaceSubtypeMem : {F : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : PartialOrder R] →
          [inst_2 : IsStrictOrderedRing R] →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : Module R M] →
                [inst_5 : SetLike F M] →
                  [AddSubmonoidClass F M] →
                    [SMulMemClass F R M] →
                      [inst_8 : Convexity.ConvexSpace R M] →
                        [Convexity.IsModuleConvexSpace R M] → (S : F) → Convexity.ConvexSpace R ↥S
-- Mathlib.Algebra.Star.SelfAdjoint
Commute.isStarNormal_add : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] [inst_1 : StarRing R] {a b : R},
  Commute a (star b) → ∀ [ha : IsStarNormal a] [hb : IsStarNormal b], IsStarNormal (a + b)
-- Init.Data.ByteArray.Basic
/-- Moves the iterator's position several bytes forward.

The resulting iterator is only valid if the number of bytes to skip is less than or equal to
the number of bytes left in the iterator.
 -/
ByteArray.Iterator.forward : ByteArray.Iterator → ℕ → ByteArray.Iterator
-- Mathlib.Data.QPF.Univariate.Basic
/-- two trees are equivalent if their F-abstractions are  -/
QPF.Wequiv : {F : Type u → Type v} → [q : QPF F] → (QPF.P F).W → (QPF.P F).W → Prop
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinite_iff_abs_lt_abs : ∀ {x : ℝ*}, x.Infinite ↔ ∀ (r : ℝ), |↑r| < |x|
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
instIsBotOneClass : ∀ {α : Type u} [inst : MulOneClass α] [inst_1 : LE α] [CanonicallyOrderedMul α], IsBotOneClass α
-- Mathlib.NumberTheory.Padics.WithVal
Padic.withValUniformEquiv_cast_apply : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (x : WithVal (Rat.padicValuation p)),
  Padic.withValUniformEquiv ↑x = ↑((WithVal.equiv (Rat.padicValuation p)) x)
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.LeftExactFunctor.forget_obj_of : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.Limits.PreservesFiniteLimits F],
  (CategoryTheory.LeftExactFunctor.forget C D).obj (CategoryTheory.LeftExactFunctor.of F) = F
-- Aesop.Index
_private.Aesop.Index.0.Aesop.Index.applicableByHypRules : {α : Type} →
  Aesop.Index α →
    Lean.MVarId → (Aesop.Rule α → Bool) → Lean.MetaM (Array (Aesop.Rule α × Array Aesop.IndexMatchLocation))
-- Init.Data.Random
/-- Generates a random Boolean.  -/
randBool : {gen : Type u} → [RandomGen gen] → gen → Bool × gen
-- Lean.Setup
Lean.instBEqIRPhases.beq : Lean.IRPhases → Lean.IRPhases → Bool
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.encard_sdiff_add_encard`. -/
Set.encard_diff_add_encard : ∀ {α : Type u_1} (s t : Set α), (s \ t).encard + t.encard = (s ∪ t).encard
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Cont'.cons₂ : Turing.PartrecToTM2.Cont' → Turing.PartrecToTM2.Cont'
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
PowerBasis.equivAdjoinSimple_symm_aeval : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (pb : PowerBasis K L)
  (f : Polynomial K),
  pb.equivAdjoinSimple.symm ((Polynomial.aeval pb.gen) f) =
    (Polynomial.aeval (IntermediateField.AdjoinSimple.gen K pb.gen)) f
-- Mathlib.Analysis.Matrix.LDL
LDL.lowerInv.congr_simp : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : LinearOrder n] [inst_2 : WellFoundedLT n]
  [inst_3 : LocallyFiniteOrderBot n] {S S_1 : Matrix n n 𝕜} (e_S : S = S_1) [inst_4 : Fintype n] (hS : S.PosDef)
  (a a_1 : n), a = a_1 → ∀ (a_2 a_3 : n), a_2 = a_3 → LDL.lowerInv hS a a_2 = LDL.lowerInv ⋯ a_1 a_3
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Multipliable.of_inv : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : CommGroup α] [inst_1 : TopologicalSpace α]
  [IsTopologicalGroup α] {f : β → α}, Multipliable (fun b => (f b)⁻¹) L → Multipliable f L
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getKeyGED_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k fallback : α},
  t₁.Equiv t₂ → t₁.getKeyGED k fallback = t₂.getKeyGED k fallback
-- Lean.Meta.ForEachExpr
/-- Given an expression `e = fun (x₁ : α₁) .. (xₙ : αₙ) => b`, runs `f` on each `αᵢ` and `b`.  -/
Lean.Meta.visitLambda : {m : Type → Type u_1} → [Monad m] → [MonadControlT Lean.MetaM m] → (Lean.Expr → m Unit) → Lean.Expr → m Unit
-- Mathlib.Geometry.Convex.Cone.Basic
/-- A pointed and salient cone defines an `IsOrderedAddMonoid`.  -/
ConvexCone.to_isOrderedAddMonoid : ∀ {R : Type u_2} {G : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup G]
  [inst_3 : SMul R G] (C : ConvexCone R G) (h₁ : C.Pointed) (h₂ : C.Salient),
  have x := C.toPartialOrder h₁ h₂;
  IsOrderedAddMonoid G
-- Init.Data.Dyadic.Basic
Dyadic.zero.sizeOf_spec : sizeOf Dyadic.zero = 1
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
AlgebraicGeometry.SheafedSpace.instEpiTopCatBaseHomPresheafedSpaceπ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasLimits C]
  {X Y : AlgebraicGeometry.SheafedSpace C} (f g : X ⟶ Y),
  CategoryTheory.Epi (CategoryTheory.Limits.coequalizer.π f g).hom.base
-- Mathlib.Combinatorics.Colex
Finset.orderIsoColex_apply : ∀ (n : ℕ), Finset.orderIsoColex n = toColex (Finset.equivBitIndices n)
-- Init.Data.SInt.Bitwise
ISize.and_eq_neg_one_iff : ∀ {a b : ISize}, a &&& b = -1 ↔ a = -1 ∧ b = -1
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The induced functor to `Over X` from a functor `J ⥤ C` and natural maps `sᵢ : X ⟶ Dᵢ`.
For the converse direction see `CategoryTheory.WithTerminal.commaFromOver`.  -/
CategoryTheory.Over.lift : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {J : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} J] →
        (D : CategoryTheory.Functor J T) →
          {X : T} → (D ⟶ (CategoryTheory.Functor.const J).obj X) → CategoryTheory.Functor J (CategoryTheory.Over X)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.map_add_one : ∀ (f : CircleDeg1Lift) (x : ℝ), f (x + 1) = f x + 1
-- Mathlib.Topology.Algebra.Module.IsWeak
/-- The evaluation map `(B · y) : E → 𝕜` is continuous for each `y : F`.  -/
LinearMap.IsWeak.continuous_eval : ∀ {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace E] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [hB : B.IsWeak] (y : F), Continuous fun x => (B x) y
-- Mathlib.Topology.Order.ScottTopology
Topology.WithScott.ofScott_inj : ∀ {α : Type u_1} {a b : Topology.WithScott α}, Topology.WithScott.ofScott a = Topology.WithScott.ofScott b ↔ a = b
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.map₂_eq_range_lift_comp_mapIncl : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {P : Type u_9} {Q : Type u_10} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid P] [inst_3 : AddCommMonoid Q] [inst_4 : Module R M] [inst_5 : Module R P]
  [inst_6 : Module R Q] (f : P →ₗ[R] Q →ₗ[R] M) (p : Submodule R P) (q : Submodule R Q),
  Submodule.map₂ f p q = (TensorProduct.lift f ∘ₗ TensorProduct.mapIncl p q).range
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.lift_comp_embed : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (S : Type u_4)
  [inst_3 : CommSemiring S] {N : Type u_5} [inst_4 : AddCommMonoid N] [inst_5 : Module R N] [inst_6 : Module S N]
  (f : M →ₗ[R] N) [inst_7 : Algebra R S] [inst_8 : IsScalarTower R S N],
  (DividedPowerAlgebra.map S f).toLinearMap ∘ₗ DividedPowerAlgebra.embed R M = ↑R (DividedPowerAlgebra.embed S N) ∘ₗ f
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.normalizedFactors_eq_of_dvd : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  (a p : α),
  p ∈ UniqueFactorizationMonoid.normalizedFactors a → ∀ q ∈ UniqueFactorizationMonoid.normalizedFactors a, p ∣ q → p = q
-- Init.PropLemmas
forall_or_imp_or_self_left_left : ∀ {α : Sort u_1} {P Q R : α → Prop}, (∀ (a : α), Q a ∨ P a → Q a ∨ R a) ↔ ∀ (a : α), P a → Q a ∨ R a
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- Constructs an isomorphism of `BinaryFan`s out of an isomorphism of the tips that commutes with
the projections.  -/
CategoryTheory.Limits.BinaryFan.ext : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A B : C} →
      {c c' : CategoryTheory.Limits.BinaryFan A B} →
        (e : c.pt ≅ c'.pt) →
          c.fst = CategoryTheory.CategoryStruct.comp e.hom c'.fst →
            c.snd = CategoryTheory.CategoryStruct.comp e.hom c'.snd → (c ≅ c')
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
Int.reduceBdiv : Lean.Meta.Simp.DSimproc
-- Std.Data.HashSet.Basic
/-- Internal implementation detail of the hash map  -/
Std.HashSet.Equiv.inner : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α}, m₁.Equiv m₂ → m₁.inner.Equiv m₂.inner
-- Init.Data.SInt.Basic
/-- Obtains the `Int32` whose 2's complement representation is the given `BitVec 32`.  -/
Int32.ofBitVec : BitVec 32 → Int32
-- Mathlib.Data.List.MinMax
List.argmax.congr_simp : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {inst_1 : DecidableLT β} [inst_2 : DecidableLT β] (f f_1 : α → β),
  f = f_1 → ∀ (l l_1 : List α), l = l_1 → List.argmax f l = List.argmax f_1 l_1
-- Lean.Server.RequestCancellation
Lean.Server.RequestCancellationToken.cancelByEdit : Lean.Server.RequestCancellationToken → BaseIO Unit
-- Std.Data.Internal.List.Associative
/-- Like `List.min?`, but using an `Ord` typeclass instead of a `Min` typeclass.  -/
Std.Internal.List.minEntry? : {α : Type u} → {β : α → Type v} → [Ord α] → List ((a : α) × β a) → Option ((a : α) × β a)
-- Mathlib.Algebra.Group.End
/-- **Alias** of `AddAut.neg_apply`. -/
AddAut.inv_apply : ∀ (M : Type u_2) [inst : Add M] (e : AddAut M) (m : M), (-e) m = (AddEquiv.symm e) m
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalRingHom.map_srange : ∀ {R : Type u} {S : Type v} {T : Type w} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  [inst_2 : NonUnitalNonAssocSemiring T] (g : S →ₙ+* T) (f : R →ₙ+* S),
  NonUnitalSubsemiring.map g (NonUnitalRingHom.srange f) = NonUnitalRingHom.srange (g.comp f)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.post.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) {D : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} D]
  [inst_3 : CategoryTheory.Limits.HasColimit F] (G : CategoryTheory.Functor C D)
  [inst_4 : CategoryTheory.Limits.HasColimit (F.comp G)],
  CategoryTheory.Limits.colimit.post F G =
    CategoryTheory.Limits.colimit.desc (F.comp G) (G.mapCocone (CategoryTheory.Limits.colimit.cocone F))
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
CategoryTheory.PreGaloisCategory.IsFundamentalGroup.toIsNaturalSMul : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{u₂, u₁} C} {F : CategoryTheory.Functor C FintypeCat}
  {inst_1 : CategoryTheory.GaloisCategory C} {G : Type u_1} {inst_2 : Group G}
  {inst_3 : (X : C) → MulAction G (F.obj X).obj} {inst_4 : TopologicalSpace G} {inst_5 : IsTopologicalGroup G}
  {inst_6 : CompactSpace G} [self : CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G],
  CategoryTheory.PreGaloisCategory.IsNaturalSMul F G
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
/-- `RelStruct` is reflexive.  -/
SSet.PtSimplex.RelStruct.refl : {X : SSet} →
  {n : ℕ} → {x : X.obj (Opposite.op { len := 0 })} → (f : X.PtSimplex n x) → (i : Fin (n + 1)) → f.RelStruct f i
-- Mathlib.Data.ENNReal.Inv
ENNReal.iInf_mul_iInf : ∀ {ι : Sort u_1} {f g : ι → ENNReal},
  (∃ i, f i ≠ ⊤) → (∃ j, g j ≠ ⊤) → (∀ (i j : ι), ∃ k, f k * g k ≤ f i * g j) → (⨅ i, f i) * ⨅ i, g i = ⨅ i, f i * g i
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.homologyIsoImageICyclesCompPOpcycles_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C),
  CategoryTheory.CategoryStruct.comp S.homologyIsoImageICyclesCompPOpcycles.hom
      (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp S.iCycles S.pOpcycles)) =
    S.homologyι
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
_private.Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol.0.ZMod.χ₈.match_1.eq_4 : ∀ (motive : ZMod 8 → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 2) (h_3 : Unit → motive 4)
  (h_4 : Unit → motive 6) (h_5 : Unit → motive 1) (h_6 : Unit → motive 7) (h_7 : Unit → motive 3)
  (h_8 : Unit → motive 5),
  (match 6 with
    | 0 => h_1 ()
    | 2 => h_2 ()
    | 4 => h_3 ()
    | 6 => h_4 ()
    | 1 => h_5 ()
    | 7 => h_6 ()
    | 3 => h_7 ()
    | 5 => h_8 ()) =
    h_4 ()
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.instInhabitedMRefinePat.default : Lean.Parser.Tactic.MRefinePat
-- Mathlib.ModelTheory.Bundled
FirstOrder.Language.Theory.ModelType.mk.sizeOf_spec : ∀ {L : FirstOrder.Language} {T : L.Theory} [inst : (a : L.Sentence) → SizeOf (T a)] (Carrier : Type w)
  [struc : L.Structure Carrier] [is_model : Carrier ⊨ T] [nonempty' : Nonempty Carrier],
  sizeOf { Carrier := Carrier, struc := struc, is_model := is_model, nonempty' := nonempty' } =
    1 + sizeOf Carrier + sizeOf struc + sizeOf is_model + sizeOf nonempty'
-- Lean.Data.Lsp.Extra
/-- `$/lean/prepareModuleHierarchy` client->server request.

Response type: `Option LeanModule`
 -/
Lean.Lsp.LeanPrepareModuleHierarchyParams : Type
-- Mathlib.Data.Finset.Range
Finset.range_eq_empty_iff : ∀ {n : ℕ}, Finset.range n = ∅ ↔ n = 0
-- Mathlib.Algebra.Algebra.Unitization
Unitization.algebraMap_eq_inl_comp : ∀ (S : Type u_1) (R : Type u_2) (A : Type u_3) [inst : CommSemiring S] [inst_1 : CommSemiring R]
  [inst_2 : NonUnitalSemiring A] [inst_3 : Module R A] [inst_4 : IsScalarTower R A A] [inst_5 : SMulCommClass R A A]
  [inst_6 : Algebra S R] [inst_7 : DistribMulAction S A] [inst_8 : IsScalarTower S R A],
  ⇑(algebraMap S (Unitization R A)) = Unitization.inl ∘ ⇑(algebraMap S R)
-- Mathlib.Data.Set.Operations
/-- **Alias** of `Set.notMem_ofPred_iff`. -/
Set.notMem_setOf_iff : ∀ {α : Type u} {a : α} {p : α → Prop}, a ∉ {x | p x} ↔ ¬p a
-- Mathlib.Analysis.Matrix.Order
Matrix.toLinearMap_tracePositiveLinearMap : ∀ (n : Type u_3) (α : Type u_4) (𝕜 : Type u_5) [inst : Fintype n] [inst_1 : Semiring α] [inst_2 : RCLike 𝕜]
  [inst_3 : Module α 𝕜], (Matrix.tracePositiveLinearMap n α 𝕜).toLinearMap = Matrix.traceLinearMap n α 𝕜
-- Mathlib.Analysis.Distribution.TemperateGrowth
/-- Given a function such that `f` and `x ^ (k + l) * f` are bounded for a suitable `l`, then
`x ^ k * f` is integrable. The bounds are not relevant for the integrability conclusion, but they
are relevant for bounding the integral in `integral_pow_mul_le_of_le_of_pow_mul_le`. We formulate
the two lemmas with the same set of assumptions for ease of applications.  -/
integrable_of_le_of_pow_mul_le : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E]
  [inst_2 : NormedAddCommGroup F] [BorelSpace E] [SecondCountableTopology E] {μ : MeasureTheory.Measure E}
  [μ.HasTemperateGrowth] {f : E → F} {C₁ C₂ : ℝ} {k : ℕ},
  (∀ (x : E), ‖f x‖ ≤ C₁) →
    (∀ (x : E), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂) →
      MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.Integrable (fun x => ‖x‖ ^ k * ‖f x‖) μ
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.exists_Spec_apply_eq : ∀ {X : AlgebraicGeometry.Scheme} (x : ↥X), ∃ R f, ∃ (_ : AlgebraicGeometry.IsOpenImmersion f), ∃ y, f y = x
-- Mathlib.FieldTheory.IsAlgClosed.Classification
/-- setting `R` to be `ZMod (ringChar R)` this result shows that if two algebraically
closed fields have equipotent transcendence bases and the same characteristic then they are
isomorphic.  -/
IsAlgClosed.equivOfTranscendenceBasis : {R : Type u_1} →
  {L : Type u_2} →
    {K : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : Field K] →
          [inst_2 : Algebra R K] →
            [inst_3 : Field L] →
              [inst_4 : Algebra R L] →
                {ι : Type u_4} →
                  (v : ι → K) →
                    {κ : Type u_5} →
                      (w : κ → L) →
                        [IsAlgClosed K] →
                          [IsAlgClosed L] → ι ≃ κ → IsTranscendenceBasis R v → IsTranscendenceBasis R w → K ≃+* L
-- Mathlib.Order.SupClosed
/-- **Alias** of the reverse direction of `latticeClosure_eq_self`. -/
IsSublattice.latticeClosure_eq : ∀ {α : Type u_3} [inst : Lattice α] {s : Set α}, IsSublattice s → latticeClosure s = s
-- Init.Prelude
/-- Unsafe auxiliary constant used by the compiler to erase `Quot.lift`.
 -/
Quot.lcInv : {α : Sort u} → {r : α → α → Prop} → Quot r → α
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.ext : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] {f g : P →ᴬ[R] Q},
  (∀ (x : P), f x = g x) → f = g
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- In a topological vector space, the addition of a measurable function and a simple function is
measurable.  -/
Measurable.add_simpleFunc : ∀ {α : Type u_1} {E : Type u_5} {x : MeasurableSpace α} [inst : MeasurableSpace E] [inst_1 : AddCancelMonoid E]
  [MeasurableAdd E] {g : α → E}, Measurable g → ∀ (f : MeasureTheory.SimpleFunc α E), Measurable (g + ⇑f)
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.inv_def : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (e : X ≃ᵈ X), e⁻¹ = e.symm
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.IsSeparatedFor.ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X},
  CategoryTheory.Presieve.IsSeparatedFor P R →
    ∀ {t₁ t₂ : P.obj (Opposite.op X)},
      (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
          R f →
            (CategoryTheory.ConcreteCategory.hom (P.map f.op)) t₁ =
              (CategoryTheory.ConcreteCategory.hom (P.map f.op)) t₂) →
        t₁ = t₂
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Hom.map_apply : ∀ {V : Type u_1} {W : Type u_2} (f : V → W) (G : SimpleGraph V) (h : ∀ {u v : V}, G.Adj u v → f u ≠ f v) (a : V),
  (SimpleGraph.Hom.map f G h) a = f a
-- Std.Data.DTreeMap.Basic
/-- Returns a map that contains all mappings of `t₁` and `t₂`. In case that both maps contain the
same key `k` with respect to `cmp`, the provided function is used to determine the new value from
the respective values in `t₁` and `t₂`.

This function ensures that `t₁` is used linearly. It also uses the individual values in `t₁`
linearly if the merge function uses the second argument (i.e. the first of type `β a`) linearly.
Hence, as long as `t₁` is unshared, the performance characteristics follow the following imperative
description: Iterate over all mappings in `t₂`, inserting them into `t₁` if `t₁` does not contain a
conflicting mapping yet. If `t₁` does contain a conflicting mapping, use the given merge function to
merge the mapping in `t₂` into the mapping in `t₁`. Then return `t₁`.

Hence, the runtime of this method scales logarithmically in the size of `t₁` and linearly in the size of
`t₂` as long as `t₁` is unshared.
 -/
Std.DTreeMap.mergeWith : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.LawfulEqCmp cmp] →
        ((a : α) → β a → β a → β a) → Std.DTreeMap α β cmp → Std.DTreeMap α β cmp → Std.DTreeMap α β cmp
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.locallyRingedSpaceObj_presheaf : ∀ (R : CommRingCat),
  (AlgebraicGeometry.Spec.locallyRingedSpaceObj R).presheaf = (AlgebraicGeometry.Spec.structureSheaf ↑R).obj
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.ne_zero_of_trailingDegree_lt : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ∞}, p.trailingDegree < n → p ≠ 0
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.isSFiniteKernel_const : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Nonempty α]
  {μβ : MeasureTheory.Measure β},
  ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.Kernel.const α μβ) ↔ MeasureTheory.SFinite μβ