mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Methods.mk.sizeOf_spec : ∀ (pre post : Lean.Meta.Simp.Simproc) (dpre dpost : Lean.Meta.Simp.DSimproc)
  (discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)) (wellBehavedDischarge : Bool),
  sizeOf
      { pre := pre, post := post, dpre := dpre, dpost := dpost, discharge? := discharge?,
        wellBehavedDischarge := wellBehavedDischarge } =
    1 + sizeOf wellBehavedDischarge
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.unop_inf : ∀ {M : Type u_2} [inst : Mul M] (S₁ S₂ : Subsemigroup Mᵐᵒᵖ), (S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
ProbabilityTheory.Kernel.partialTraj_zero : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} {a : ℕ}
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))},
  ProbabilityTheory.Kernel.partialTraj κ a 0 = ProbabilityTheory.Kernel.deterministic (Preorder.frestrictLe₂ ⋯) ⋯
-- Mathlib.RingTheory.IsAdjoinRoot
/-- `AdjoinRoot f` is indeed given by adjoining a root of `f`.  -/
AdjoinRoot.isAdjoinRoot : {R : Type u} → [inst : CommRing R] → (f : Polynomial R) → IsAdjoinRoot (AdjoinRoot f) f
-- Mathlib.LinearAlgebra.UnitaryGroup
/-- The `Matrix.map star` of a unitary matrix (i.e., taking the `star` of
each element in the matrix) as a unitary matrix.  -/
Matrix.UnitaryGroup.map_star : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      {α : Type v} →
        [inst_2 : CommRing α] → [inst_3 : StarRing α] → ↥(Matrix.unitaryGroup n α) → ↥(Matrix.unitaryGroup n α)
-- Mathlib.RingTheory.PicardGroup
Module.Flat.instSubtypeMemSubmoduleSubmoduleAlgebra : ∀ {R : Type u} {M : Type v} {A : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (e : TensorProduct R A M ≃ₗ[A] A) [Module.Flat R M] [FaithfulSMul R A],
  Module.Flat R ↥(Module.Flat.submoduleAlgebra e)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.right_inv_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  (X : C) [self : CategoryTheory.GrpObj X] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id X) CategoryTheory.GrpObj.inv)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h)
-- Mathlib.RingTheory.IsAdjoinRoot
/-- If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`.  -/
IsAdjoinRootMonic.mkOfAdjoinEqTop : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          [IsDomain R] →
            [IsDomain S] →
              [Module.IsTorsionFree R S] →
                [IsIntegrallyClosed R] → {α : S} → IsIntegral R α → R[α] = ⊤ → IsAdjoinRootMonic S (minpoly R α)
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.regular.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A : C)
  [inst_2 : CategoryTheory.AddMonObj A],
  CategoryTheory.AddMod.regular A = { X := A, addMod := CategoryTheory.AddModObj.regular A }
-- Mathlib.Data.Seq.Computation
Computation.of_think_mem : ∀ {α : Type u} {s : Computation α} {a : α}, a ∈ s.think → a ∈ s
-- Mathlib.Algebra.GroupWithZero.Action.End
/-- Compose a `DistribMulAction` with a `MonoidHom`, with action `f r' • m`.
See note [reducible non-instances].  -/
DistribMulAction.compHom : {M : Type u_1} →
  {N : Type u_2} →
    (A : Type u_3) →
      [inst : AddMonoid A] →
        [inst_1 : Monoid M] → [DistribMulAction M A] → [inst_3 : Monoid N] → (N →* M) → DistribMulAction N A
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  [inst_1 : SizeOf C] (base : C) (fiber : ↑(F.obj base)),
  sizeOf { base := base, fiber := fiber } = 1 + sizeOf base + sizeOf fiber
-- Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries
/-- The power series $\sum_{k=-\infty}^{\infty}(-1)^k x^{k * (3k - 1) / 2}$.  -/
PowerSeries.pentagonalSeries : (R : Type u_1) → [CommRing R] → PowerSeries R
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.instIsRegularMonoι : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (g h : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair g h)],
  CategoryTheory.IsRegularMono (CategoryTheory.Limits.equalizer.ι g h)
-- Mathlib.Algebra.Group.Commute.Defs
Commute.pow_self : ∀ {M : Type u_2} [inst : Monoid M] (a : M) (n : ℕ), Commute (a ^ n) a
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.u₄_eq_one_or_neg_one : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
  FermatLastTheoremForThreeGen.Solution.u₄✝ S = 1 ∨ FermatLastTheoremForThreeGen.Solution.u₄✝ S = -1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_insertₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k}
  {l : Std.DTreeMap.Internal.Impl α β} (hlb : l.Balanced),
  l.Ordered →
    (Std.DTreeMap.Internal.Impl.insertₘ k v l hlb).toListModel.Perm (Std.Internal.List.insertEntry k v l.toListModel)
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.rename_monomial : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ → τ) [inst : Filter.TendstoCofinite f] [inst_1 : CommSemiring R]
  (x : σ →₀ ℕ) (r : R),
  (MvPowerSeries.rename f) ((MvPowerSeries.monomial x) r) = (MvPowerSeries.monomial (Finsupp.mapDomain f x)) r
-- Mathlib.Data.List.Range
List.ranges.eq_1 : [].ranges = []
-- Mathlib.Topology.Algebra.UniformConvergence
instCommGroupUniformOnFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : CommGroup β],
  instCommGroupUniformOnFun = { toGroup := instGroupUniformOnFun, mul_comm := ⋯ }
-- Lean.Parser.Extra
Lean.Parser.hygieneInfo.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.List.Perm
List.Perm.append_left : ∀ {α : Type u_1} {t₁ t₂ : List α} (l : List α), t₁.Perm t₂ → (l ++ t₁).Perm (l ++ t₂)
-- Mathlib.LinearAlgebra.Complex.Module
/-- Create a `selfAdjoint` element from a `skewAdjoint` element by multiplying by the scalar
`-Complex.I`.  -/
skewAdjoint.negISMul : {A : Type u_1} →
  [inst : AddCommGroup A] →
    [inst_1 : Module ℂ A] →
      [inst_2 : StarAddMonoid A] → [inst_3 : StarModule ℂ A] → ↥(skewAdjoint A) →ₗ[ℝ] ↥(selfAdjoint A)
-- Batteries.Data.Nat.Lemmas
Nat.add_mul_lt_mul_of_lt_of_lt : ∀ {m n x y : ℕ}, x < m → y < n → x + m * y < m * n
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.isEmpty_insertMany_list : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : List α}, (m.insertMany l).isEmpty = (m.isEmpty && l.isEmpty)
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_X_pow_sub_C : ∀ {R : Type u} [inst : Ring R] [Nontrivial R] {n : ℕ} {r : R}, (Polynomial.X ^ n - Polynomial.C r).natDegree = n
-- Mathlib.Data.Sigma.Basic
Function.Surjective.sigma_map : ∀ {α₁ : Type u_2} {α₂ : Type u_3} {β₁ : α₁ → Type u_5} {β₂ : α₂ → Type u_6} {f₁ : α₁ → α₂}
  {f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)},
  Function.Surjective f₁ → (∀ (a : α₁), Function.Surjective (f₂ a)) → Function.Surjective (Sigma.map f₁ f₂)
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.fieldId.inj : ∀ {stx : Lean.Syntax} {id : Option Lean.Name} {lctx : Lean.LocalContext} {structName : Lean.Name} {stx_1 : Lean.Syntax}
  {id_1 : Option Lean.Name} {lctx_1 : Lean.LocalContext} {structName_1 : Lean.Name},
  Lean.Elab.CompletionInfo.fieldId stx id lctx structName =
      Lean.Elab.CompletionInfo.fieldId stx_1 id_1 lctx_1 structName_1 →
    stx = stx_1 ∧ id = id_1 ∧ lctx = lctx_1 ∧ structName = structName_1
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
CochainComplex.Plus.instHasRightResolutionsArrowInjectiveObjectArrowInverseImageQuasiIsoMapCochainComplexPlusιArrowLocalizerMorphism : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.EnoughInjectives C], (CochainComplex.Plus.localizerMorphism C).arrow.HasRightResolutions
-- Mathlib.Data.DFinsupp.NeLocus
DFinsupp.neLocus_add_left : ∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst_1 : (a : α) → DecidableEq (N a)]
  [inst_2 : (a : α) → AddLeftCancelMonoid (N a)] (f g h : Π₀ (a : α), N a), (f + g).neLocus (f + h) = g.neLocus h
-- Mathlib.CategoryTheory.Action.Limits
Action.instReflectsLimitsForget : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G],
  CategoryTheory.Limits.ReflectsLimits (Action.forget V G)
-- Mathlib.Computability.NFA
NFA.append_mem_acceptsFrom : ∀ {α : Type u} {σ : Type v} (M : NFA α σ) {S : Set σ} {x y : List α},
  x ++ y ∈ M.acceptsFrom S ↔ y ∈ M.acceptsFrom (M.evalFrom S x)
-- Mathlib.Order.Filter.AtTopBot.Finset
/-- `Finset.card` tends to `pure (Fintype.card α)`, when `α` is finite.  -/
Filter.tendsto_card_atTop_pure_of_fintype : ∀ {α : Type u_3} [inst : Fintype α], Filter.Tendsto Finset.card Filter.atTop (pure (Fintype.card α))
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Affine.Simplex.median_map : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [CharZero k] {V₂ : Type u_4} {P₂ : Type u_5} [inst_5 : AddCommGroup V₂]
  [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] {n : ℕ} [inst_8 : NeZero n] (s : Affine.Simplex k P n)
  (i : Fin (n + 1)) (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f),
  (s.map f hf).median i = AffineSubspace.map f (s.median i)
-- Init.Data.SInt.Lemmas
Int16.le_iff_toBitVec_sle : ∀ {a b : Int16}, a ≤ b ↔ a.toBitVec.sle b.toBitVec = true
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.ker_liftQ : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  {R₂ : Type u_3} {M₂ : Type u_4} [inst_3 : Ring R₂] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ f.ker), (p.liftQ f h).ker = Submodule.map p.mkQ f.ker
-- Mathlib.Analysis.Complex.Norm
Complex.norm_map_zero' : ‖0‖ = 0
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.counitIso_inv_hom_id_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) (Y : D),
  CategoryTheory.CategoryStruct.comp (e.counitInv.app Y) (e.counit.app Y) = CategoryTheory.CategoryStruct.id Y
-- Mathlib.RingTheory.AdjoinRoot
/-- Lift a ring homomorphism `i : R →+* S` to `AdjoinRoot f →+* S`.  -/
AdjoinRoot.lift : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      {f : Polynomial R} →
        [inst_1 : CommRing S] → (i : R →+* S) → (x : S) → Polynomial.eval₂ i x f = 0 → AdjoinRoot f →+* S
-- Mathlib.Data.Nat.Choose.Multinomial
Multiset.multinomial_add : ∀ (m m' : Multiset ℕ), (m + m').multinomial = (m + m').sum.choose m.sum * m.multinomial * m'.multinomial
-- Mathlib.Analysis.Calculus.FDeriv.Prod
DifferentiableWithinAt.fderivWithin_prodMk : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f₁ : E → F} {x : E} {s : Set E} {f₂ : E → G},
  DifferentiableWithinAt 𝕜 f₁ s x →
    DifferentiableWithinAt 𝕜 f₂ s x →
      UniqueDiffWithinAt 𝕜 s x →
        fderivWithin 𝕜 (fun x => (f₁ x, f₂ x)) s x = (fderivWithin 𝕜 f₁ s x).prod (fderivWithin 𝕜 f₂ s x)
-- Lean.Util.NumObjs
Lean.Expr.NumObjs.main : Lean.Expr → ℕ
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.allM_mapM : ∀ {α β β' : Type w} {m : Type w → Type w'} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad m]
  [inst_3 : MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] {it : Std.Iter β} {f : β → m β'}
  {p : β' → m (ULift.{w, 0} Bool)},
  Std.IterM.allM p (Std.Iter.mapM f it) =
    Std.IterM.allM
      (fun x => do
        let __do_lift ← f x
        p __do_lift)
      (Std.Iter.mapM pure it)
-- Mathlib.Topology.Category.TopCat.GrothendieckTopology
TopCat.isOpenEmbedding_iff : ∀ {X Y : TopCat} (f : X ⟶ Y),
  TopCat.isOpenEmbedding f ↔ Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
HasSum.of_sigma : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : UniformSpace α] [IsUniformAddGroup α]
  {γ : β → Type u_4} {f : (b : β) × γ b → α} {g : β → α} {a : α},
  (∀ (b : β), HasSum (fun c => f ⟨b, c⟩) (g b)) → HasSum g a → (CauchySeq fun s => ∑ i ∈ s, f i) → HasSum f a
-- Mathlib.Algebra.GroupWithZero.Defs
CancelMonoidWithZero.mk.inj : ∀ {M₀ : Type u_2} {toMonoidWithZero : MonoidWithZero M₀} {toIsCancelMulZero : IsCancelMulZero M₀}
  {toMonoidWithZero_1 : MonoidWithZero M₀} {toIsCancelMulZero_1 : IsCancelMulZero M₀},
  { toMonoidWithZero := toMonoidWithZero, toIsCancelMulZero := toIsCancelMulZero } =
      { toMonoidWithZero := toMonoidWithZero_1, toIsCancelMulZero := toIsCancelMulZero_1 } →
    toMonoidWithZero = toMonoidWithZero_1
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
because it is a composition of multiple projections.  -/
LinearIsometryEquiv.Simps.apply : {R : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : Semiring R₂] →
        (σ₁₂ : R →+* R₂) →
          {σ₂₁ : R₂ →+* R} →
            [inst_2 : RingHomInvPair σ₁₂ σ₂₁] →
              [inst_3 : RingHomInvPair σ₂₁ σ₁₂] →
                (E : Type u_11) →
                  (E₂ : Type u_12) →
                    [inst_4 : SeminormedAddCommGroup E] →
                      [inst_5 : SeminormedAddCommGroup E₂] →
                        [inst_6 : Module R E] → [inst_7 : Module R₂ E₂] → (E ≃ₛₗᵢ[σ₁₂] E₂) → E → E₂
-- Mathlib.Lean.Name
/-- Decapitalize the last component of a name.  -/
Lean.Name.decapitalize : Lean.Name → Lean.Name
-- Mathlib.Algebra.Category.Ring.Colimits
_private.Mathlib.Algebra.Category.Ring.Colimits.0.RingCat.Colimits.descFunLift.match_1.splitter : {J : Type u_1} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J RingCat) →
      (motive : RingCat.Colimits.Prequotient F → Sort u_2) →
        (x : RingCat.Colimits.Prequotient F) →
          ((j : J) → (x : ↑(F.obj j)) → motive (RingCat.Colimits.Prequotient.of j x)) →
            (Unit → motive RingCat.Colimits.Prequotient.zero) →
              (Unit → motive RingCat.Colimits.Prequotient.one) →
                ((x : RingCat.Colimits.Prequotient F) → motive x.neg) →
                  ((x y : RingCat.Colimits.Prequotient F) → motive (x.add y)) →
                    ((x y : RingCat.Colimits.Prequotient F) → motive (x.mul y)) → motive x
-- Mathlib.Topology.Algebra.Monoid
instContinuousAddOrderDual : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Add M] [ContinuousAdd M], ContinuousAdd Mᵒᵈ
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
/-- Since `Real.smoothTransition` is constant on $(-∞, 0]$ and $[1, ∞)$, applying it to the
projection of `x : ℝ` to $[0, 1]$ gives the same result as applying it to `x`.  -/
Real.smoothTransition.projIcc : ∀ {x : ℝ}, (↑(Set.projIcc 0 1 ⋯ x)).smoothTransition = x.smoothTransition
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (self : CategoryTheory.Pseudofunctor B C) →
          {a b c : B} →
            (f : a ⟶ b) →
              (g : b ⟶ c) →
                self.map (CategoryTheory.CategoryStruct.comp f g) ≅
                  CategoryTheory.CategoryStruct.comp (self.map f) (self.map g)
-- Mathlib.CategoryTheory.Monoidal.Opposite.Mon
MonObj.mopEquiv_inverse_obj_X : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (M : CategoryTheory.Mon Cᴹᵒᵖ), ((MonObj.mopEquiv C).inverse.obj M).X = M.X.unmop
-- Mathlib.CategoryTheory.Category.Pointed
typeToPointed_obj_point : ∀ (X : Type u), (typeToPointed.obj X).point = none
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpIndL1Fin_smul' : ∀ {α : Type u_1} {F : Type u_2} {𝕜 : Type u_6} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {hm : m ≤ m0}
  [inst_3 : MeasureTheory.SigmaFinite (μ.trim hm)] [inst_4 : NormedSpace ℝ F] [SMulCommClass ℝ 𝕜 F]
  (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (c : 𝕜) (x : F),
  MeasureTheory.condExpIndL1Fin hm hs hμs (c • x) = c • MeasureTheory.condExpIndL1Fin hm hs hμs x
-- Mathlib.RingTheory.Localization.BaseChange
/-- The natural isomorphism `S ⊗[R] A[M⁻¹] ≃ (S ⊗[R] A)[M⁻¹]`.  -/
IsLocalization.tensorProductEquivOfMapIncludeRight : (R : Type u_7) →
  (S : Type u_8) →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          {A : Type u_9} →
            [inst_3 : CommSemiring A] →
              [inst_4 : Algebra R A] →
                (M : Submonoid A) →
                  (B : Type u_10) →
                    [inst_5 : CommSemiring B] →
                      [inst_6 : Algebra R B] →
                        [inst_7 : Algebra A B] →
                          [IsScalarTower R A B] →
                            [IsLocalization M B] →
                              (C : Type u_11) →
                                [inst_10 : CommSemiring C] →
                                  [inst_11 : Algebra S C] →
                                    [inst_12 : Algebra (TensorProduct R S A) C] →
                                      [IsScalarTower S (TensorProduct R S A) C] →
                                        [IsLocalization (Submonoid.map Algebra.TensorProduct.includeRight M) C] →
                                          TensorProduct R S B ≃ₐ[S] C
-- Mathlib.Topology.Sheaves.Presheaf
/-- If `f : X ⟶ Y` is an open map and `ℱ` is a presheaf on `Y`, then the pullback of `ℱ` by `f` is
isomorphic to the composition of `ℱ` and of the functor `(Open X)ᵒᵖ ⥤ (Open Y)ᵒᵖ` induced by `f`.
 -/
IsOpenMap.pullbackObjIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasColimits C] →
      {X Y : TopCat} →
        {f : X ⟶ Y} →
          (hf : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) →
            (ℱ : TopCat.Presheaf C Y) → (TopCat.Presheaf.pullback C f).obj ℱ ≅ hf.functor.op.comp ℱ
-- Mathlib.Data.ENat.Lattice
ENat.sSup_eq_zero : ∀ {s : Set ℕ∞}, sSup s = 0 ↔ ∀ a ∈ s, a = 0
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.normalizer_singleton : ∀ {G : Type u_1} [inst : Group G] (g : G), Subgroup.normalizer {g} = Subgroup.centralizer {g}
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castSucc_uIoo_castSucc : ∀ {n : ℕ} (i j : Fin n), Fin.castSucc ⁻¹' Set.uIoo i.castSucc j.castSucc = Set.uIoo i j
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.sections.match_1.eq_2 : ∀ {α : Type u_1} (motive : List (List α) → Sort u_2) (l : List α) (L : List (List α)) (h_1 : Unit → motive [])
  (h_2 : (l : List α) → (L : List (List α)) → motive (l :: L)),
  (match l :: L with
    | [] => h_1 ()
    | l :: L => h_2 l L) =
    h_2 l L
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.any_eq_true_iff_exists_mem_get : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  {p : (a : α) → β a → Bool}, m.any p = true ↔ ∃ a, ∃ (h : a ∈ m), p a (m.get a h) = true
-- Mathlib.Order.LiminfLimsup
OrderIso.liminf_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_6} [inst : ConditionallyCompleteLattice β]
  [inst_1 : ConditionallyCompleteLattice γ] {f : Filter α} {u : α → β} (g : β ≃o γ),
  autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) OrderIso.liminf_apply._auto_1 →
    autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f u) OrderIso.liminf_apply._auto_3 →
      autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f fun x => g (u x)) OrderIso.liminf_apply._auto_5 →
        autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f fun x => g (u x)) OrderIso.liminf_apply._auto_7 →
          g (Filter.liminf u f) = Filter.liminf (fun x => g (u x)) f
-- Std.Do.PredTrans
Std.Do.PredTrans.mk.sizeOf_spec : ∀ {ps : Std.Do.PostShape} {α : Type u} [inst : SizeOf α] (trans : Std.Do.PostCond α ps → Std.Do.Assertion ps)
  (conjunctiveRaw : Std.Do.PredTrans.Conjunctive trans), sizeOf { trans := trans, conjunctiveRaw := conjunctiveRaw } = 1
-- Mathlib.Data.Int.Init
/-- See `Int.inductionOn'` for an induction in both directions.  -/
Int.leInductionDown : {m : ℤ} →
  {motive : (n : ℤ) → n ≤ m → Sort u_1} →
    motive m ⋯ → ((n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯) → (n : ℤ) → (hnm : n ≤ m) → motive n hnm
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
HasStrictDerivAt.cosh : ∀ {f : ℝ → ℝ} {f' x : ℝ}, HasStrictDerivAt f f' x → HasStrictDerivAt (fun x => Real.cosh (f x)) (Real.sinh (f x) * f') x
-- Mathlib.Algebra.Ring.Subsemiring.Pointwise
Subsemiring.smul_closure : ∀ {M : Type u_1} {R : Type u_2} [inst : Monoid M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] (a : M)
  (s : Set R), a • Subsemiring.closure s = Subsemiring.closure (a • s)
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ShortComplex.mapToComposableArrows_app_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂),
  (CategoryTheory.ShortComplex.mapToComposableArrows φ).app 1 = φ.τ₂
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.restr_coe : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set α), ↑(e.restr s) = ↑e
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.IsUniversal.uniq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {f g : CategoryTheory.CostructuredArrow S T} (h : f.IsUniversal) (η : g ⟶ f),
  η = CategoryTheory.Limits.IsTerminal.from h g
-- Std.Do.Internal.Ensures.Lemmas
/-- `MayReturn` is equivalent to `MonadAttach.CanReturn` for `LawfulMonadAttach` instances.  -/
Std.Do.Internal.MayReturn.canReturn_iff : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] [LawfulMonad m] [inst_2 : MonadAttach m]
  [LawfulMonadAttach m] (x : m α) (a : α), MonadAttach.CanReturn x a ↔ Std.Do.Internal.MayReturn x a
-- Mathlib.Condensed.Explicit
/-- A `CondensedMod` version of `Condensed.ofSheafStonean`.  -/
CondensedMod.ofSheafStonean : (R : Type (u + 1)) →
  [inst : Ring R] →
    (F : CategoryTheory.Functor Stoneanᵒᵖ (ModuleCat R)) →
      [CategoryTheory.Limits.PreservesFiniteProducts F] → CondensedMod R
-- Mathlib.Algebra.Order.Archimedean.Defs
exists_lt_pow : ∀ {R : Type u_1} [inst : CommMonoid R] [inst_1 : PartialOrder R] [MulLeftStrictMono R] [MulArchimedean R] {a : R},
  1 < a → ∀ (b : R), ∃ n, b < a ^ n
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.ι₁_snd_assoc : ∀ (X : SSet) {Z : SSet} (h : SSet.stdSimplex.obj { len := 1 } ⟶ Z),
  CategoryTheory.CategoryStruct.comp SSet.ι₁
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.SemiCartesianMonoidalCategory.snd X (SSet.stdSimplex.obj { len := 1 })) h) =
    CategoryTheory.CategoryStruct.comp (SSet.const (SSet.stdSimplex.obj₀Equiv.symm 1)) h