mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.EmbeddingOfLocal
/-- Consider a vector space `E` over a `NontriviallyNormedField` `𝕜`, and `t₁`, `t₂` two
vector space topologies on `E`.

Assume that there is a `t₁`-neighborhood of zero `V` such that the two topogies induce the
same filter of neighborhoods of `0` *in the subspace `V`*. Then `t₁ = t₂`.  -/
ContinuousSMul.topology_eq_of_nhds_inf_principal_eq : ∀ (𝕜₁ : Type u_1) {E : Type u_3} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜₁ E]
  (t₁ t₂ : TopologicalSpace E) [IsTopologicalAddGroup E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜₁ E]
  [ContinuousSMul 𝕜₁ E] {V : Set E}, V ∈ nhds 0 → nhds 0 ⊓ Filter.principal V = nhds 0 ⊓ Filter.principal V → t₁ = t₂
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
/-- `a : α` is a Stieltjes point for `f : α → ℚ → ℝ` if `f a` is monotone with limit 0 at -∞
and 1 at +∞ and satisfies a continuity property.  -/
ProbabilityTheory.IsRatStieltjesPoint : {α : Type u_1} → (α → ℚ → ℝ) → α → Prop
-- Mathlib.CategoryTheory.Abelian.Refinements
CategoryTheory.ShortComplex.liftCycles_comp_homologyπ_eq_iff_up_to_refinements : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S : CategoryTheory.ShortComplex C} {A : C} (x₂ x₂' : A ⟶ S.X₂) (hx₂ : CategoryTheory.CategoryStruct.comp x₂ S.g = 0)
  (hx₂' : CategoryTheory.CategoryStruct.comp x₂' S.g = 0),
  CategoryTheory.CategoryStruct.comp (S.liftCycles x₂ hx₂) S.homologyπ =
      CategoryTheory.CategoryStruct.comp (S.liftCycles x₂' hx₂') S.homologyπ ↔
    ∃ A' π,
      ∃ (_ : CategoryTheory.Epi π),
        ∃ x₁,
          CategoryTheory.CategoryStruct.comp π x₂ =
            CategoryTheory.CategoryStruct.comp π x₂' + CategoryTheory.CategoryStruct.comp x₁ S.f
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α} {v : β}, a ∈ t.insert k v ↔ cmp k a = Ordering.eq ∨ a ∈ t
-- Mathlib.Order.Interval.Set.ProjIcc
Set.projIcc_of_right_le : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α} (h : a ≤ b) {x : α}, b ≤ x → Set.projIcc a b h x = ⟨b, ⋯⟩
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalExpr.instList : {α : Type} → [Lean.Elab.ConfigEval.EvalExpr α] → Lean.Elab.ConfigEval.EvalExpr (List α)
-- Mathlib.Algebra.Algebra.Unitization
/-- If `φ : A →⋆ₙₐ[R] B` is surjective, the lift
`starMap φ : Unitization R A →⋆ₐ[R] Unitization R B` is also surjective.  -/
Unitization.starMap_surjective : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : NonUnitalSemiring A] [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : SMulCommClass R A A]
  [inst_6 : IsScalarTower R A A] [inst_7 : NonUnitalSemiring B] [inst_8 : StarRing B] [inst_9 : Module R B]
  [inst_10 : SMulCommClass R B B] [inst_11 : IsScalarTower R B B] [inst_12 : StarModule R B] {φ : A →⋆ₙₐ[R] B},
  Function.Surjective ⇑φ → Function.Surjective ⇑(Unitization.starMap φ)
-- Mathlib.Order.Filter.AtTopBot.Archimedean
atBot_isCountablyGenerated_of_archimedean : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [IsOrderedRing R] [Archimedean R],
  Filter.atBot.IsCountablyGenerated
-- Std.Sat.AIG.LawfulVecOperator
Std.Sat.AIG.LawfulVecOperator.denote_mem_prefix : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Std.Sat.AIG α → ℕ → Type}
  {f : {len : ℕ} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len}
  [inst_2 : Std.Sat.AIG.LawfulVecOperator α β fun {len} => f] {len : ℕ} {assign : α → Bool} {start : ℕ} {inv : Bool}
  {aig : Std.Sat.AIG α} {input : β aig len} (h : start < aig.decls.size),
  ⟦assign, { aig := (f aig input).aig, ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := { gate := start, invert := inv, hgate := h } }⟧
-- Mathlib.Data.Sum.Basic
Sum.LiftRel.exists_of_isRight_right : ∀ {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s : β → δ → Prop} {x : α ⊕ β} {y : γ ⊕ δ},
  Sum.LiftRel r s x y → y.isRight = true → ∃ b d, s b d ∧ x = Sum.inr b ∧ y = Sum.inr d
-- Mathlib.Data.Finsupp.Basic
Finsupp.comapDomain.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f f_1 : α → β) (e_f : f = f_1) (l l_1 : β →₀ M)
  (e_l : l = l_1) (hf : Set.InjOn f (f ⁻¹' ↑l.support)), Finsupp.comapDomain f l hf = Finsupp.comapDomain f_1 l_1 ⋯
-- Init.Grind.Ordered.Module
Lean.Grind.ExistsAddOfLT : (α : Type u) → [LT α] → [Zero α] → [Add α] → Prop
-- Mathlib.Topology.Bornology.Basic
Bornology.isBounded_insert : ∀ {α : Type u_2} {x : Bornology α} {s : Set α} {x_1 : α}, Bornology.IsBounded (insert x_1 s) ↔ Bornology.IsBounded s
-- Mathlib.Algebra.Homology.HomotopyCategory
HomotopyCategory.instFaithfulFunctorHomologicalComplexObjWhiskeringLeftQuotient : ∀ {ι : Type u_2} (V : Type u) [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  (c : ComplexShape ι) {D : Type u_3} [inst_2 : CategoryTheory.Category.{v_1, u_3} D],
  ((CategoryTheory.Functor.whiskeringLeft (HomologicalComplex V c) (HomotopyCategory V c) D).obj
      (HomotopyCategory.quotient V c)).Faithful
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Cofan.ext_inv_hom : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : β → C}
  {c₁ c₂ : CategoryTheory.Limits.Cofan f} (e : c₁.pt ≅ c₂.pt)
  (w :
    autoParam (∀ (b : β), CategoryTheory.CategoryStruct.comp (c₁.inj b) e.hom = c₂.inj b)
      CategoryTheory.Limits.Cofan.ext._auto_1),
  (CategoryTheory.Limits.Cofan.ext e w).inv.hom = e.inv
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Returns the first non-`none` result of applying the monadic function `f` to each output
of the iterator, in order. Returns `none` if `f` returns `none` for all outputs.

`O(|it|)`. Short-circuits when `f` returns `some _`. The outputs of `it` are
examined in order of iteration.

This function is deprecated. Instead of `it.allowNontermination.findSomeM?`, use `it.findSomeM?`.

Example:
```lean example
#eval ([7, 6, 5, 8, 1, 2, 6].iterM IO).findSomeM? fun i => do
  if i < 5 then
    return some (i * 10)
  if i ≤ 6 then
    IO.println s!"Almost! {i}"
  return none
```
```output
Almost! 6
Almost! 5
```
```output
some 10
```
 -/
Std.IterM.Partial.findSomeM? : {α β γ : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] → [Std.IteratorLoop α m m] → Std.IterM.Partial m β → (β → m (Option γ)) → m (Option γ)
-- Mathlib.Logic.Equiv.Sum
Equiv.sumEmpty_symm_apply : ∀ (α : Type u_9) (β : Type u_10) [inst : IsEmpty β] (val : α), (Equiv.sumEmpty α β).symm val = Sum.inl val
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
PresheafOfModules.Derivation.Universal.fac : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
  {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ : S ⟶ F.op.comp R}
  {d : M.Derivation φ} (self : d.Universal)
  {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (d' : M'.Derivation φ),
  d.postcomp (self.desc d') = d'
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.smul_iso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  (a : ℤˣ) (e : X ≅ Y), (a • e).inv = a⁻¹ • e.inv
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
/-- Homotopic refinements induce the same map on multiequalizers.  -/
CategoryTheory.PreOneHypercover.Homotopy.mapMultiforkOfIsLimit_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {A : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} A] {E F : CategoryTheory.PreOneHypercover S} {f g : E.Hom F}
  (H : CategoryTheory.PreOneHypercover.Homotopy f g) (P : CategoryTheory.Functor Cᵒᵖ A)
  {c : CategoryTheory.Limits.Multifork (E.multicospanIndex P)} (hc : CategoryTheory.Limits.IsLimit c)
  (d : CategoryTheory.Limits.Multifork (F.multicospanIndex P)),
  f.mapMultiforkOfIsLimit P hc d = g.mapMultiforkOfIsLimit P hc d
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_erase_self : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α}, (m.erase k).getKey? k = none
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getThenInsertIfNew?_fst : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {k : α} {v : β k}, (m.getThenInsertIfNew? k v).1 = m.get? k
-- Std.Data.DTreeMap.Internal.Operations
/-- Slower version of `modify` which can be used in the absence of balance
information but still assumes the preconditions of `modify`, otherwise might panic.
 -/
Std.DTreeMap.Internal.Impl.alter! : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      [Std.LawfulEqOrd α] →
        (k : α) → (Option (β k) → Option (β k)) → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.tryCatch_ReaderT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ε : Type u_1} {α ρ : Type u} {x : ReaderT ρ m α}
  {h : ε → ReaderT ρ m α} [inst : Std.Do.WP m ps] [inst_1 : MonadExceptOf ε m]
  (Q : Std.Do.PostCond α (Std.Do.PostShape.arg ρ ps)),
  ⦃fun r => (Std.Do.wp (MonadExceptOf.tryCatch (x.run r) fun e => (h e).run r)).apply (fun a => Q.1 a r, Q.2)⦄
    MonadExceptOf.tryCatch x h ⦃Q⦄
-- Mathlib.Topology.Covering.Basic
IsEvenlyCovered.toTrivialization.eq_1 : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {I : Type u_3}
  [inst_2 : TopologicalSpace I] {x : X} [inst_3 : Nonempty I] (h : IsEvenlyCovered f x I),
  h.toTrivialization = h.toTrivialization'.transFiberHomeomorph h.fiberHomeomorph
-- Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
EuclideanSpace.volume_closedBall_fin_two : ∀ (x : EuclideanSpace ℝ (Fin 2)) (r : ℝ),
  MeasureTheory.volume (Metric.closedBall x r) = ENNReal.ofReal r ^ 2 * ENNReal.ofReal Real.pi
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
DifferentiableOn.csin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {s : Set E},
  DifferentiableOn ℂ f s → DifferentiableOn ℂ (fun x => Complex.sin (f x)) s
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
AlgebraicTopology.AlternatingCofaceMapComplex.d_squared : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.CosimplicialObject C) (n : ℕ),
  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.AlternatingCofaceMapComplex.objD X n)
      (AlgebraicTopology.AlternatingCofaceMapComplex.objD X (n + 1)) =
    0
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.inv_fun_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) (X Y : C) (f : X ⟶ Y),
  e.inverse.map (e.functor.map f) =
    CategoryTheory.CategoryStruct.comp (e.unitInv.app X) (CategoryTheory.CategoryStruct.comp f (e.unit.app Y))
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey?_eq_some_minKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  (he : t ≠ ∅), t.minKey? = some (t.minKey he)
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- Reinterpret a linear isometry as an affine isometry.  -/
LinearIsometry.toAffineIsometry : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {V₂ : Type u_5} →
      [inst : NormedField 𝕜] →
        [inst_1 : SeminormedAddCommGroup V] →
          [inst_2 : NormedSpace 𝕜 V] →
            [inst_3 : SeminormedAddCommGroup V₂] → [inst_4 : NormedSpace 𝕜 V₂] → (V →ₗᵢ[𝕜] V₂) → V →ᵃⁱ[𝕜] V₂
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
/-- **Uniqueness of the conditional expectation**
If a function is a.e. `m`-measurable, verifies an integrability condition and has same integral
as `f` on all `m`-measurable sets, then it is a.e. equal to `μ[f|hm]`.  -/
MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq : ∀ {α : Type u_1} {E : Type u_3} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] (hm : m ≤ m₀) [MeasureTheory.SigmaFinite (μ.trim hm)] {f g : α → E},
  MeasureTheory.Integrable f μ →
    (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn g s μ) →
      (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, f x ∂μ) →
        MeasureTheory.AEStronglyMeasurable g μ → g =ᵐ[μ] μ[f | m]
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.nonempty_cellFrontier`. -/
Topology.CWComplex.nonempty_cellFrontier : ∀ {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [inst : Topology.CWComplex C] {n : ℕ},
  n ≠ 0 → ∀ (j : Topology.RelCWComplex.cell C n), (Topology.RelCWComplex.cellFrontier n j).Nonempty
-- Mathlib.Algebra.Group.Conj
addConjugatesOf.eq_1 : ∀ {α : Type u} [inst : AddMonoid α] (a : α), addConjugatesOf a = {b | IsAddConj a b}
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_of_isEmpty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {a : α}, m.isEmpty = true → m.getKey! a = default
-- Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
differentiableWithinAt_iff_restrictScalars : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' E] [inst_6 : IsScalarTower 𝕜 𝕜' E] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
  [inst_8 : NormedSpace 𝕜 F] [inst_9 : NormedSpace 𝕜' F] [inst_10 : IsScalarTower 𝕜 𝕜' F] {f : E → F} {s : Set E}
  {x : E},
  DifferentiableWithinAt 𝕜 f s x →
    UniqueDiffWithinAt 𝕜 s x →
      (DifferentiableWithinAt 𝕜' f s x ↔ ∃ g', ContinuousLinearMap.restrictScalars 𝕜 g' = fderivWithin 𝕜 f s x)
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normalCore_eq_iInf_comap_addConj : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.normalCore = ⨅ g, AddSubgroup.comap (↑(AddAut.addConj g)) H
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.of_zero : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} [inst : Zero A], CStarMatrix.ofMatrix 0 = 0
-- Mathlib.Data.ENNReal.BigOperators
ENNReal.iInf_sum : ∀ {ι : Type u_3} {α : Type u_4} {f : ι → α → ENNReal} {s : Finset α} [Nonempty ι],
  (∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a) → ⨅ i, ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ i, f i a
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
_private.Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives.0.HomotopyCategory.Plus.isRightDerivabilityStructure.instIsLocalizedEquivalencePlusQuasiIsoQuasiIsoR : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C],
  (HomotopyCategory.Plus.isRightDerivabilityStructure.R✝ C).IsLocalizedEquivalence
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.isBlock_iff_smul_eq_smul_of_nonempty : ∀ {G : Type u_1} {X : Type u_2} [inst : SMul G X] {B : Set X},
  MulAction.IsBlock G B ↔ ∀ ⦃g₁ g₂ : G⦄, (g₁ • B ∩ g₂ • B).Nonempty → g₁ • B = g₂ • B
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.addGrp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (self : CategoryTheory.AddGrp C) → CategoryTheory.AddGrpObj self.X
-- Mathlib.Analysis.Analytic.CPolynomialDef
HasFiniteFPowerSeriesAt.hasFPowerSeriesAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {n : ℕ}, HasFiniteFPowerSeriesAt f p x n → HasFPowerSeriesAt f p x
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch.getElem_eq : ∀ {pat s : ByteArray} {needlePos stackPos : ℕ}
  (self : String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat s needlePos stackPos) (j : ℕ)
  (hj : j < needlePos), pat[j] = s[stackPos - needlePos + j]
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.associator_inv_left_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂}
  [inst_9 : CategoryTheory.Category.{v₁₀, u₁₀} A'''] [inst_10 : CategoryTheory.Category.{v₁₁, u₁₁} B''']
  [inst_11 : CategoryTheory.Category.{v₁₂, u₁₂} C'''] {F''' : CategoryTheory.Functor A''' B'''}
  {G''' : CategoryTheory.Functor C''' B'''} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G')
  (φ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G'')
  (φ'' : CategoryTheory.Limits.CatCospanTransform F'' G'' F''' G''') (x : A),
  (φ.associator φ' φ'').inv.left.app x = CategoryTheory.CategoryStruct.id (φ''.left.obj (φ'.left.obj (φ.left.obj x)))
-- Mathlib.GroupTheory.CommutingProbability
DihedralGroup.reciprocalFactors_odd : ∀ {n : ℕ}, n ≠ 1 → Odd n → DihedralGroup.reciprocalFactors n = n % 4 * n :: DihedralGroup.reciprocalFactors (n / 4 + 1)
-- Mathlib.Logic.Function.Defs
Function.prod_comp_fst_comp_snd : ∀ {α₁ : Type u_4} {α₂ : Type u_5} {β₁ : Type u_6} {β₂ : Type u_7} (f : α₁ → α₂) (g : β₁ → β₂),
  Function.prod (f ∘ Prod.fst) (g ∘ Prod.snd) = Prod.map f g
-- Std.Data.DTreeMap.Internal.Queries
/-- Folds the given function over the mappings in the tree in descending order.  -/
Std.DTreeMap.Internal.Impl.foldr : {α : Type u} → {β : α → Type v} → {δ : Type w} → ((a : α) → β a → δ → δ) → δ → Std.DTreeMap.Internal.Impl α β → δ
-- Init.Data.SInt.Lemmas
Int16.instIsLinearOrder : Std.IsLinearOrder Int16
-- Mathlib.Algebra.Field.Defs
DivisionRing.mk : {K : Type u_2} →
  [toRing : Ring K] →
    [toInv : Inv K] →
      [toDiv : Div K] →
        [toZPow : ZPow K] →
          autoParam (∀ (a b : K), a / b = a * b⁻¹) DivInvMonoid.div_eq_mul_inv._autoParam →
            autoParam (∀ (a : K), a ^ 0 = 1) DivInvMonoid.zpow_zero'._autoParam →
              autoParam (∀ (n : ℕ) (a : K), a ^ ↑n.succ = a ^ ↑n * a) DivInvMonoid.zpow_succ'._autoParam →
                autoParam (∀ (n : ℕ) (a : K), a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹) DivInvMonoid.zpow_neg'._autoParam →
                  [toNontrivial : Nontrivial K] →
                    [toNNRatCast : NNRatCast K] →
                      [toRatCast : RatCast K] →
                        (∀ (a : K), a ≠ 0 → a * a⁻¹ = 1) →
                          0⁻¹ = 0 →
                            autoParam (∀ (q : ℚ≥0), ↑q = ↑q.num / ↑q.den) DivisionRing.nnratCast_def._autoParam →
                              (nnqsmul : ℚ≥0 → K → K) →
                                autoParam (∀ (q : ℚ≥0) (a : K), nnqsmul q a = ↑q * a)
                                    DivisionRing.nnqsmul_def._autoParam →
                                  autoParam (∀ (q : ℚ), ↑q = ↑q.num / ↑q.den) DivisionRing.ratCast_def._autoParam →
                                    (qsmul : ℚ → K → K) →
                                      autoParam (∀ (a : ℚ) (x : K), qsmul a x = ↑a * x)
                                          DivisionRing.qsmul_def._autoParam →
                                        DivisionRing K
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
/-- `X₁ ×[Y₁] (X₂ ×[Y₂] X₃)` is the pullback `(X₁ ×[Y₁] X₂) ×[Y₂] X₃`.  -/
CategoryTheory.Limits.pullbackAssocSymmIsPullback : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ Y₁ Y₂ : C} →
      (f₁ : X₁ ⟶ Y₁) →
        (f₂ : X₂ ⟶ Y₁) →
          (f₃ : X₂ ⟶ Y₂) →
            (f₄ : X₃ ⟶ Y₂) →
              [inst_1 : CategoryTheory.Limits.HasPullback f₁ f₂] →
                [inst_2 : CategoryTheory.Limits.HasPullback f₃ f₄] →
                  [inst_3 :
                      CategoryTheory.Limits.HasPullback f₁
                        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)] →
                    CategoryTheory.Limits.IsLimit
                      (CategoryTheory.Limits.PullbackCone.mk
                        (CategoryTheory.Limits.pullback.lift
                          (CategoryTheory.Limits.pullback.fst f₁
                            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂))
                          (CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.Limits.pullback.snd f₁
                              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂))
                            (CategoryTheory.Limits.pullback.fst f₃ f₄))
                          ⋯)
                        (CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.Limits.pullback.snd f₁
                            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂))
                          (CategoryTheory.Limits.pullback.snd f₃ f₄))
                        ⋯)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.natDegree_preΨ'_pos : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) {n : ℕ}, 2 < n → ↑n ≠ 0 → 0 < (W.preΨ' n).natDegree
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.neg_apply : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : (i : ι) → Neg (G i)] (f : (i : ι) → G i) (i : ι), (-f) i = -f i
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Mathlib.Meta.Positivity.log_nonneg_of_isNat : ∀ {e : ℝ} {n : ℕ}, Mathlib.Meta.NormNum.IsNat e n → 0 ≤ Real.log e
-- Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
CategoryTheory.ShiftedHom.opEquiv_symm_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] {X Y Z : C}
  {a b : ℤ} (f : CategoryTheory.ShiftedHom (Opposite.op Z) (Opposite.op Y) a)
  (g : CategoryTheory.ShiftedHom (Opposite.op Y) (Opposite.op X) b) {c : ℤ} (h : b + a = c),
  (CategoryTheory.ShiftedHom.opEquiv c).symm (f.comp g h) =
    ((CategoryTheory.ShiftedHom.opEquiv b).symm g).comp ((CategoryTheory.ShiftedHom.opEquiv a).symm f) ⋯
-- Mathlib.NumberTheory.ModularForms.QExpansion
_private.Mathlib.NumberTheory.ModularForms.QExpansion.0.UpperHalfPlane.hasSum_cuspFunction_of_hasSum_punctured : ∀ {h : ℝ} {f : UpperHalfPlane → ℂ},
  0 < h →
    ∀ {c : ℕ → ℂ},
      (∀ (τ : UpperHalfPlane), HasSum (fun m => c m • Function.Periodic.qParam h ↑τ ^ m) (f τ)) →
        ∀ {q : ℂ}, ‖q‖ < 1 → q ≠ 0 → HasSum (fun m => c m • q ^ m) (UpperHalfPlane.cuspFunction h f q)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstr.mk.sizeOf_spec : ∀ (p : Int.Internal.Linear.Poly) (h : Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof),
  sizeOf { p := p, h := h } = 1 + sizeOf p + sizeOf h