mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
_private.Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis.0.Tactic.ComputeAsymptotics.BasisExtension.getBasis.match_1.eq_1 : ∀ (motive : (basis : Tactic.ComputeAsymptotics.Basis) → Tactic.ComputeAsymptotics.BasisExtension basis → Sort u_1)
  (h_1 : Unit → motive [] Tactic.ComputeAsymptotics.BasisExtension.nil)
  (h_2 :
    (basis_hd : ℝ → ℝ) →
      (basis_tl : Tactic.ComputeAsymptotics.Basis) →
        (ex : Tactic.ComputeAsymptotics.BasisExtension basis_tl) →
          motive (basis_hd :: basis_tl) (Tactic.ComputeAsymptotics.BasisExtension.keep basis_hd ex))
  (h_3 :
    (basis : Tactic.ComputeAsymptotics.Basis) →
      (f : ℝ → ℝ) →
        (ex : Tactic.ComputeAsymptotics.BasisExtension basis) →
          motive basis (Tactic.ComputeAsymptotics.BasisExtension.insert f ex)),
  (match [], Tactic.ComputeAsymptotics.BasisExtension.nil with
    | .([]), Tactic.ComputeAsymptotics.BasisExtension.nil => h_1 ()
    | .(basis_hd :: basis_tl), Tactic.ComputeAsymptotics.BasisExtension.keep basis_hd ex => h_2 basis_hd basis_tl ex
    | basis, Tactic.ComputeAsymptotics.BasisExtension.insert f ex => h_3 basis f ex) =
    h_1 ()
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.of_isPushout : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C}
  [self : P.IsStableUnderCobaseChange] {A A' B B' : C} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'},
  CategoryTheory.IsPushout g f f' g' → P f → P f'
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  k ∉ m₁ → (m₁ \ m₂).get? k = none
-- Init.Data.Int.DivMod.Lemmas
Int.divExact_eq_tdiv : ∀ {a b : ℤ} (h : b ∣ a), a.divExact b h = a.tdiv b
-- Aesop.RuleSet.Member
Aesop.LocalRuleSetMember.toGlobalRuleSetMember? : Aesop.LocalRuleSetMember → Option Aesop.GlobalRuleSetMember
-- Mathlib.Logic.Equiv.Embedding
_private.Mathlib.Logic.Equiv.Embedding.0.Equiv.sumEmbeddingEquivProdEmbeddingDisjoint.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : α ⊕ β → Sort u_3) →
      (x : α ⊕ β) → ((a : α) → motive (Sum.inl a)) → ((b : β) → motive (Sum.inr b)) → motive x
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.toEquiv : {X : Type u_1} → {Y : Type u_2} → [inst : PseudoEMetricSpace X] → [inst_1 : PseudoEMetricSpace Y] → X ≃ᵈ Y → X ≃ Y
-- Mathlib.Tactic.NormNum.Basic
/-- The `norm_num` extension which identifies expressions of the form `(a : ℕ) | b`,
such that `norm_num` successfully recognises both `a` and `b`.  -/
Mathlib.Meta.NormNum.evalNatDvd : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.smulCommClass_left : ∀ {K : Type u} [inst : DivisionRing K] {X : Type u_2} {Y : Type u_1} [inst_1 : SMul K Y] [inst_2 : SMul X Y]
  [SMulCommClass K X Y] (F : Subfield K), SMulCommClass (↥F) X Y
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.map_injective : ∀ {ι : Type u_3} {α : ι → Type u_4} {β : ι → Type u_5} [inst : (i : ι) → AddCommMonoid (α i)]
  [inst_1 : (i : ι) → AddCommMonoid (β i)] (f : (i : ι) → α i →+ β i),
  Function.Injective ⇑(DirectSum.map f) ↔ ∀ (i : ι), Function.Injective ⇑(f i)
-- Mathlib.Logic.Equiv.Basic
Equiv.piCongr'_apply : ∀ {α : Sort u_1} {β : Sort u_4} {W : α → Sort w} {Z : β → Sort z} (h₁ : α ≃ β) (h₂ : (b : β) → W (h₁.symm b) ≃ Z b)
  (f : (a : α) → W a), (h₁.piCongr' h₂) f = fun b => (h₂ b) (f (h₁.symm b))
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The cofork `biprod.inrCokernelFork` is indeed a colimit.  -/
CategoryTheory.Limits.biprod.isCokernelInrCokernelFork : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (X Y : C) →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] →
          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.biprod.inrCokernelCofork X Y)
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
ContinuousLinearEquiv.uniformConvergenceCLMCongr_symm_apply : ∀ {𝕜 : Type u_6} {E : Type u_7} {F : Type u_8} {G : Type u_9} {H : Type u_10} [inst : AddCommGroup E]
  [inst_1 : AddCommGroup F] [inst_2 : AddCommGroup G] [inst_3 : AddCommGroup H] [inst_4 : NormedField 𝕜]
  [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜 F] [inst_7 : Module 𝕜 G] [inst_8 : Module 𝕜 H] [inst_9 : TopologicalSpace E]
  [inst_10 : TopologicalSpace F] [inst_11 : TopologicalSpace G] [inst_12 : TopologicalSpace H]
  [inst_13 : IsTopologicalAddGroup G] [inst_14 : IsTopologicalAddGroup H] [inst_15 : ContinuousConstSMul 𝕜 G]
  [inst_16 : ContinuousConstSMul 𝕜 H] (e₁ : E ≃L[𝕜] F) (e₂ : H ≃L[𝕜] G) (𝔖 : Set (Set E)) (𝔗 : Set (Set F))
  (h : ∀ (t : Set F), t ∈ 𝔗 ↔ ⇑e₁ ⁻¹' t ∈ 𝔖) (φ : UniformConvergenceCLM (RingHom.id 𝕜) G 𝔗) (e : E),
  ((e₁.uniformConvergenceCLMCongr e₂ 𝔖 𝔗 h).symm φ) e = e₂.symm (φ (e₁ e))
-- Init.Data.String.Lemmas.Basic
String.push_empty : ∀ {c : Char}, "".push c = String.singleton c
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.RootPositiveForm.mk.inj : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} {inst : CommRing S}
  {inst_1 : LinearOrder S} {inst_2 : CommRing R} {inst_3 : Algebra S R} {inst_4 : AddCommGroup M} {inst_5 : Module R M}
  {inst_6 : AddCommGroup N} {inst_7 : Module R N} {P : RootPairing ι R M N} {inst_8 : P.IsValuedIn S}
  {form : LinearMap.BilinForm R M} {symm : LinearMap.IsSymm form}
  {isOrthogonal_reflection : ∀ (i : ι), LinearMap.IsOrthogonal form ⇑(P.reflection i)}
  {exists_eq : ∀ (i j : ι), ∃ s, (algebraMap S R) s = (form (P.root i)) (P.root j)}
  {exists_pos_eq : ∀ (i : ι), ∃ s > 0, (algebraMap S R) s = (form (P.root i)) (P.root i)}
  {form_1 : LinearMap.BilinForm R M} {symm_1 : LinearMap.IsSymm form_1}
  {isOrthogonal_reflection_1 : ∀ (i : ι), LinearMap.IsOrthogonal form_1 ⇑(P.reflection i)}
  {exists_eq_1 : ∀ (i j : ι), ∃ s, (algebraMap S R) s = (form_1 (P.root i)) (P.root j)}
  {exists_pos_eq_1 : ∀ (i : ι), ∃ s > 0, (algebraMap S R) s = (form_1 (P.root i)) (P.root i)},
  { form := form, symm := symm, isOrthogonal_reflection := isOrthogonal_reflection, exists_eq := exists_eq,
        exists_pos_eq := exists_pos_eq } =
      { form := form_1, symm := symm_1, isOrthogonal_reflection := isOrthogonal_reflection_1, exists_eq := exists_eq_1,
        exists_pos_eq := exists_pos_eq_1 } →
    form = form_1
-- Mathlib.Algebra.Group.Subsemigroup.Operations
MulHom.domRestrict.eq_1 : ∀ {M : Type u_1} {σ : Type u_4} [inst : Mul M] {N : Type u_5} [inst_1 : Mul N] [inst_2 : SetLike σ M]
  [inst_3 : MulMemClass σ M] (f : M →ₙ* N) (S : σ), f.domRestrict S = f.comp (MulMemClass.subtype S)
-- Lean.Elab.Term.TermElabM
/-- If `e? = some e`, then `tryPostponeIfMVar e`, otherwise it is just `tryPostpone`.  -/
Lean.Elab.Term.tryPostponeIfNoneOrMVar : Option Lean.Expr → Lean.Elab.TermElabM Unit
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- `PreservesLimitsOfSize_shrink.{w w'} F` tries to obtain `PreservesLimitsOfSize.{w w'} F`
from some other `PreservesLimitsOfSize F`.
 -/
CategoryTheory.Limits.preservesLimitsOfSize_shrink : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesLimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.Order.Filter.Lift
Filter.sInter_lift'_sets : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {h : Set α → Set β}, Monotone h → ⋂₀ {s | s ∈ f.lift' h} = ⋂ s ∈ f, h s
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Extract
Std.Tactic.BVDecide.BVExpr.bitblast.ExtractTarget.mk.sizeOf_spec : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {len : ℕ} [inst_2 : SizeOf α] {w : ℕ}
  (vec : aig.RefVec w) (start : ℕ),
  sizeOf { w := w, vec := vec, start := start } = 1 + sizeOf w + sizeOf vec + sizeOf start
-- Mathlib.CategoryTheory.Subobject.Basic
/-- Use choice to pick a representative underlying object in `C` for any `Subobject X`.

Prefer to use the coercion `P : C` rather than explicitly writing `underlying.obj P`.
 -/
CategoryTheory.Subobject.underlying : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {X : C} → CategoryTheory.Functor (CategoryTheory.Subobject X) C
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedMethods : Inhabited Lean.Meta.Grind.Methods
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
DifferentiableAt.ccosh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E},
  DifferentiableAt ℂ f x → DifferentiableAt ℂ (fun x => Complex.cosh (f x)) x
-- Mathlib.Algebra.Ring.Hom.Defs
/-- Ring homomorphisms map one to one.  -/
RingHom.map_one : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), f 1 = 1
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.ComposableArrows.mapFunctorArrows.congr_simp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (i j i' j' n : ℕ) (x : i ≤ j) (x_1 : i' ≤ j') (x_2 : i ≤ i')
  (x_3 : j ≤ j') (x_4 : j' ≤ n),
  CategoryTheory.ComposableArrows.mapFunctorArrows C i j i' j' n x x_1 x_2 x_3 x_4 =
    CategoryTheory.ComposableArrows.mapFunctorArrows C i j i' j' n x x_1 x_2 x_3 x_4
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_preimage_smul : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : Group G] [inst_1 : MulAction G α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.SMulInvariantMeasure G α μ] (c : G) (s : Set α),
  μ ((fun x => c • x) ⁻¹' s) = μ s
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.isubtree.eq_1 : ∀ {F : PFunctor.{uA, uB}} [inst : DecidableEq F.A] [inst_1 : Inhabited F.M] (x : F.M), PFunctor.M.isubtree [] x = x
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.logSizeRadius_le_card_smallBall : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [inst_1 : DecidableEq T] (hJ : J.Nonempty)
  (i : ℕ),
  1 < a →
    (if (PairReduction.logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) *
        a ^ ((PairReduction.logSizeBallSeq J hJ a c i).radius - 1) ≤
      ↑((PairReduction.logSizeBallSeq J hJ a c i).smallBall c).card
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- In a balanced category, if a short complex `S` is exact and `S.g` is an epi, then
`S.X₃` is the cokernel of `S.g`.  -/
CategoryTheory.ShortComplex.Exact.gIsCokernel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S : CategoryTheory.ShortComplex C} →
        [CategoryTheory.Balanced C] →
          S.Exact →
            [CategoryTheory.Epi S.g] → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.insertList.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l : List ((a : α) × β a)), Std.Internal.List.insertList l [] = l
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Replicate
Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate.go_get : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (n curr : ℕ) (hcurr : curr ≤ n)
  (input : aig.RefVec w) (s : aig.RefVec (w * curr)) (idx : ℕ) (hidx1 : idx < w * n),
  w * curr ≤ idx →
    (Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate.go n input curr hcurr s).get idx hidx1 = input.get (idx % w) ⋯
-- Mathlib.Analysis.Convex.Side
Affine.Simplex.wOppSide_affineSpan_faceOpposite_point_left_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {n : ℕ}
  [inst_6 : NeZero n] (s : Affine.Simplex R P n) {w : Fin (n + 1) → R},
  ∑ j, w j = 1 →
    ∀ {i : Fin (n + 1)},
      (affineSpan R (Set.range (s.faceOpposite i).points)).WOppSide (s.points i)
          ((Finset.affineCombination R Finset.univ s.points) w) ↔
        w i ≤ 0
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.lcompₛₗ.congr_simp : ∀ {R : Type u_14} {R₂ : Type u_15} {R₃ : Type u_16} (R₅ : Type u_18) {M : Type u_19} {N : Type u_20} (P : Type u_21)
  [inst : Semiring R] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : Semiring R₅] {σ₁₂ : R →+* R₂}
  (σ₂₃ : R₂ →+* R₃) {σ₁₃ : R →+* R₃} [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P]
  [inst_7 : Module R M] [inst_8 : Module R₂ N] [inst_9 : Module R₃ P] [inst_10 : Module R₅ P]
  [inst_11 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_12 : SMulCommClass R₃ R₅ P] (f f_1 : M →ₛₗ[σ₁₂] N),
  f = f_1 → LinearMap.lcompₛₗ R₅ P σ₂₃ f = LinearMap.lcompₛₗ R₅ P σ₂₃ f_1
-- Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
/-- **Integration by parts for Fréchet derivatives**
Version with a scalar function: `∫ f • g' = - ∫ f' • g` when `f • g'` and `f' • g` and `f • g`
are integrable, where `f'` and `g'` are the derivatives of `f` and `g` in a given direction `v`.  -/
integral_smul_fderiv_eq_neg_fderiv_smul_of_integrable : ∀ {E : Type u_1} {G : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup G]
  [inst_3 : NormedSpace ℝ G] [inst_4 : MeasurableSpace E] {μ : MeasureTheory.Measure E} [BorelSpace E]
  [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] {𝕜 : Type u_5} [inst_8 : NormedField 𝕜] [inst_9 : NormedAlgebra ℝ 𝕜]
  [inst_10 : NormedSpace 𝕜 G] [IsScalarTower ℝ 𝕜 G] {f : E → 𝕜} {g : E → G} {v : E},
  MeasureTheory.Integrable (fun x => (fderiv ℝ f x) v • g x) μ →
    MeasureTheory.Integrable (fun x => f x • (fderiv ℝ g x) v) μ →
      MeasureTheory.Integrable (fun x => f x • g x) μ →
        (∀ x ∈ tsupport g, DifferentiableAt ℝ f x) →
          (∀ x ∈ tsupport f, DifferentiableAt ℝ g x) →
            ∫ (x : E), f x • (fderiv ℝ g x) v ∂μ = -∫ (x : E), (fderiv ℝ f x) v • g x ∂μ
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofNat_mul_im : ∀ {K : Type u_1} [inst : RCLike K] (n : ℕ) [inst_1 : n.AtLeastTwo] (z : K),
  RCLike.im (OfNat.ofNat n * z) = OfNat.ofNat n * RCLike.im z
-- Mathlib.GroupTheory.Index
Subgroup.FiniteIndex.mk : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.index ≠ 0 → H.FiniteIndex
-- Mathlib.Data.List.Basic
List.append_right_injective : ∀ {α : Type u} (s : List α), Function.Injective fun t => s ++ t
-- Mathlib.Data.EReal.Basic
instZeroEReal : Zero EReal
-- Mathlib.RingTheory.Flat.LocallyFree
Module.bijective_of_surjective_of_rankAtStalk_eq : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} {N : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [Module.Finite R M] [Module.Flat R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N] [Module.Finite R N]
  [Module.Flat R N] {φ : M →ₗ[R] N},
  Function.Surjective ⇑φ →
    (∀ (m : Ideal R) [inst_9 : m.IsMaximal],
        Module.rankAtStalk M { asIdeal := m, isPrime := ⋯ } = Module.rankAtStalk N { asIdeal := m, isPrime := ⋯ }) →
      Function.Bijective ⇑φ
-- Lean.Parser.Term
Lean.Parser.Command.plainDocComment.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.isPositive_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (T : E →ₗ[𝕜] E), T.IsPositive ↔ T.IsSymmetric ∧ ∀ (x : E), 0 ≤ inner 𝕜 (T x) x
-- Mathlib.Algebra.Algebra.Basic
Module.algebraMap_end_apply : ∀ (R : Type u) (S : Type v) (M : Type w) [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : Module S M] [inst_5 : SMulCommClass S R M] [inst_6 : SMul R S]
  [inst_7 : IsScalarTower R S M] (a : R) (m : M), ((algebraMap R (Module.End S M)) a) m = a • m
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- The action map  -/
CategoryTheory.AddMonObj.«termδ[_]» : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.Arcosh
/-- This holds for `Ioi 0` instead of only `Ici 1` due to junk values.  -/
Real.strictMonoOn_arcosh : StrictMonoOn Real.arcosh (Set.Ioi 0)
-- Mathlib.CategoryTheory.Monoidal.Center
/-- Auxiliary definition for the `MonoidalCategory` instance on `Center C`.  -/
CategoryTheory.Center.associator : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (X Y Z : CategoryTheory.Center C) → (X.tensorObj Y).tensorObj Z ≅ X.tensorObj (Y.tensorObj Z)
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.isInt_negOfNat_eq : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {a : A} {lit : ℕ},
  Mathlib.Meta.NormNum.IsInt a (Int.negOfNat lit) → a = (algebraMap R A) ((Int.negOfNat lit).rawCast + 0) + 0
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.extend_some : ∀ {n : ℕ} (c : OrderedFinpartition n) (i : Fin c.length), c.extend (some i) = c.extendMiddle i
-- Init.Data.List.Lemmas
List.eq_nil_of_append_eq_nil : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ ++ l₂ = [] → l₁ = [] ∧ l₂ = []
-- Mathlib.Algebra.Ring.Subring.Pointwise
Subring.pointwise_smul_subset_iff : ∀ {M : Type u_1} {R : Type u_2} [inst : Group M] [inst_1 : Ring R] [inst_2 : MulSemiringAction M R] {a : M}
  {S T : Subring R}, a • S ≤ T ↔ S ≤ a⁻¹ • T
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- If `X ⟶ Y` is an open immersion, and `Y` is a LocallyRingedSpace, then so is `X`.  -/
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace : {X : AlgebraicGeometry.PresheafedSpace CommRingCat} →
  (Y : AlgebraicGeometry.LocallyRingedSpace) →
    (f : X ⟶ Y.toPresheafedSpace) →
      [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] → AlgebraicGeometry.LocallyRingedSpace
-- Mathlib.RingTheory.DividedPowers.Basic
DividedPowers.ofRingEquiv.eq_1 : ∀ {A : Type u_1} {B : Type u_2} [inst : CommSemiring A] {I : Ideal A} [inst_1 : CommSemiring B] {J : Ideal B}
  {e : A ≃+* B} (h : Ideal.map e I = J) (hI : DividedPowers I),
  DividedPowers.ofRingEquiv h hI =
    { dpow := fun n b => e (hI.dpow n (e.symm b)), dpow_null := ⋯, dpow_zero := ⋯, dpow_one := ⋯, dpow_mem := ⋯,
      dpow_add := ⋯, dpow_mul := ⋯, mul_dpow := ⋯, dpow_comp := ⋯ }
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.sum_isBasis_iff : ∀ {α : Type u} {β : Type v} {M : Matroid α} {N : Matroid β} {I X : Set (α ⊕ β)},
  (M.sum N).IsBasis I X ↔ M.IsBasis (Sum.inl ⁻¹' I) (Sum.inl ⁻¹' X) ∧ N.IsBasis (Sum.inr ⁻¹' I) (Sum.inr ⁻¹' X)
-- Mathlib.Algebra.LinearRecurrence
/-- The nth coordinate of a solution in the basis equals its nth value  -/
LinearRecurrence.repr_basis_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (E : LinearRecurrence R) (u : ↥E.solSpace) (n : Fin E.order),
  (E.basis.repr u) n = ↑u ↑n
-- Std.Time.DateTime.PlainDateTime
/-- Subtracts an `Hour.Offset` from a `PlainDateTime`, adjusting the date if the hour underflows.
 -/
Std.Time.PlainDateTime.subHours : Std.Time.PlainDateTime → Std.Time.Hour.Offset → Std.Time.PlainDateTime
-- Mathlib.Computability.ContextFreeGrammar
/-- Add extra prefix to context-free producing.  -/
ContextFreeGrammar.Produces.append_left : ∀ {T : Type u_1} {g : ContextFreeGrammar T} {v w : List (Symbol T g.NT)},
  g.Produces v w → ∀ (p : List (Symbol T g.NT)), g.Produces (p ++ v) (p ++ w)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.size_ofList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α},
  List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → (Std.ExtTreeSet.ofList l cmp).size = l.length
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.ConeMorphism.map_w_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C}
  {c c' : CategoryTheory.Limits.Cone F} (f : c ⟶ c') (G : CategoryTheory.Functor C D) (j : J) {Z : D}
  (h : G.obj (F.obj j) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.map f.hom) (CategoryTheory.CategoryStruct.comp (G.map (c'.π.app j)) h) =
    CategoryTheory.CategoryStruct.comp (G.map (c.π.app j)) h
-- Mathlib.Data.Set.Monotone
strictAntiOn_insert_iff_of_forall_ge : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α} {a : α},
  (∀ x ∈ s, a ≤ x) → (StrictAntiOn f (insert a s) ↔ (∀ b ∈ s, a < b → f b < f a) ∧ StrictAntiOn f s)
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_add_const : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.AEStronglyMeasurable X μ →
    ∀ (c : ℝ), ProbabilityTheory.variance (fun ω => X ω + c) μ = ProbabilityTheory.variance X μ
-- Mathlib.Order.Category.BddOrd
BddOrd.mk.sizeOf_spec : ∀ (toPartOrd : PartOrd) [isBoundedOrder : BoundedOrder ↑toPartOrd],
  sizeOf { toPartOrd := toPartOrd, isBoundedOrder := isBoundedOrder } = 1 + sizeOf toPartOrd + sizeOf isBoundedOrder
-- Mathlib.Algebra.DirectSum.Module
/-- The linear map constructed using the universal property of the coproduct.  -/
DirectSum.toModule : (R : Type u) →
  [inst : Semiring R] →
    (ι : Type v) →
      {M : ι → Type w} →
        [inst_1 : (i : ι) → AddCommMonoid (M i)] →
          [inst_2 : (i : ι) → Module R (M i)] →
            [DecidableEq ι] →
              (N : Type u₁) →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R N] → ((i : ι) → M i →ₗ[R] N) → (DirectSum ι fun i => M i) →ₗ[R] N
-- Init.Data.Rat.Lemmas
Rat.div_def : ∀ (a b : ℚ), a / b = a * b⁻¹
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_shiftLeft' : ∀ {w₁ w₂ : ℕ} {x : BitVec w₁} {y : BitVec w₂} {i : ℕ},
  (x <<< y).getLsbD i = (decide (i < w₁) && !decide (i < y.toNat) && x.getLsbD (i - y.toNat))
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
/-- Left-whiskering in the bicategory `BasedCategory` is given by whiskering the underlying functors
and natural transformations.  -/
CategoryTheory.BasedCategory.whiskerLeft : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {𝒳 : CategoryTheory.BasedCategory 𝒮} →
      {𝒴 : CategoryTheory.BasedCategory 𝒮} →
        {𝒵 : CategoryTheory.BasedCategory 𝒮} →
          (F : CategoryTheory.BasedFunctor 𝒳 𝒴) →
            {G H : CategoryTheory.BasedFunctor 𝒴 𝒵} → (G ⟶ H) → (F.comp G ⟶ F.comp H)
-- Mathlib.Probability.ConditionalProbability
/-- A version of the law of total probability.  -/
ProbabilityTheory.cond_add_cond_compl_eq : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {s t : Set Ω},
  MeasurableSet s →
    ∀ (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ], μ[t | s] * μ s + μ[t | sᶜ] * μ sᶜ = μ t
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicAt.mul : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {x : 𝕜} {f g : 𝕜 → 𝕜'}, MeromorphicAt f x → MeromorphicAt g x → MeromorphicAt (f * g) x
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.map_zero : ∀ {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] (f : ZeroHom M N), f 0 = 0
-- Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
MeasureTheory.eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ : ∀ {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ε}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {q : ℝ},
  0 < q → MeasureTheory.eLpNorm' f q μ ≤ MeasureTheory.eLpNormEssSup f μ * μ Set.univ ^ (1 / q)
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.val_assemble₃_le : ∀ {w x y : UInt8} {c : Char}, ByteArray.utf8DecodeChar?.assemble₃ w x y = some c → c.val ≤ 65535
-- Mathlib.Order.RelIso.Basic
/-- **Alias** of `RelEmbedding.antisymm`. -/
RelEmbedding.isAntisymm : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (x : r ↪r s) [Std.Antisymm s], Std.Antisymm r
-- Mathlib.GroupTheory.Divisible
/-- An `AddMonoid A` is `α`-divisible iff `n • _` is a surjective function, i.e. the
constructive version implies the textbook approach.  -/
divisibleByOfSMulRightSurj : (A : Type u_1) →
  (α : Type u_2) →
    [inst : AddMonoid A] →
      [inst_1 : SMul α A] →
        [inst_2 : Zero α] → (∀ {n : α}, n ≠ 0 → Function.Surjective fun a => n • a) → DivisibleBy A α