mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Folds a function over an iterator from the left, accumulating a value starting with `init`.
The accumulated value is combined with the each element of the list in order, using `f`.

It is equivalent to `it.toList.foldl`.

This function is deprecated. Instead of `it.allowNontermination.fold`, use `it.fold`.
 -/
Std.IterM.Partial.fold : {m : Type w → Type w'} →
  {α β γ : Type w} →
    [Monad m] → [inst : Std.Iterator α m β] → [Std.IteratorLoop α m m] → (γ → β → γ) → γ → Std.IterM.Partial m β → m γ
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.isProbabilityMeasure_comap_down : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.comap ULift.down μ)
-- Mathlib.Data.Num.Prime
_private.Mathlib.Data.Num.Prime.0.PosNum.minFac.match_1.eq_1 : ∀ (motive : PosNum → Sort u_1) (h_1 : Unit → motive PosNum.one) (h_2 : (a : PosNum) → motive a.bit0)
  (h_3 : (n : PosNum) → motive n.bit1),
  (match PosNum.one with
    | PosNum.one => h_1 ()
    | a.bit0 => h_2 a
    | n.bit1 => h_3 n) =
    h_1 ()
-- Lean.Expr
_private.Lean.Expr.0.Lean.Expr.updateConst!Impl : Lean.Expr → List Lean.Level → Lean.Expr
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.eRank_reindex : ∀ {m : Type um} {n₀ : Type un₀} {R : Type uR} {m₀ : Type um} {n : Type un} [inst : Semiring R] (A : Matrix m n R)
  (em : m ≃ m₀) (en : n ≃ n₀), ((Matrix.reindex em en) A).eRank = A.eRank
-- Mathlib.Analysis.Normed.Module.FiniteDimension
lipschitzExtensionConstant_pos : ∀ (E' : Type u_1) [inst : NormedAddCommGroup E'] [inst_1 : NormedSpace ℝ E'] [inst_2 : FiniteDimensional ℝ E'],
  0 < lipschitzExtensionConstant E'
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.instIsRelIffEmbeddingDown'Add : ∀ {A : Type u_3} [inst : AddCommSemigroup A] [inst_1 : IsRightCancelAdd A] (a b : A),
  (ComplexShape.embeddingDown'Add a b).IsRelIff
-- Mathlib.Data.Rel
SetRel.inv_eq_self_iff : ∀ {α : Type u_1} {R : SetRel α α}, R.inv = R ↔ R.IsSymm
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_eq_zero_iff_of_nonneg_ae : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  0 ≤ᵐ[μ] f → MeasureTheory.Integrable f μ → (∫ (x : α), f x ∂μ = 0 ↔ f =ᵐ[μ] 0)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv_assoc : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (e : X ≅ Y) (y : ↑Y.toTopCat) {Z : CommRingCat}
  (h : Y.presheaf.stalk y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap e.hom ((CategoryTheory.ConcreteCategory.hom e.inv.base) y))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap e.inv y) h) =
    CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯) h
-- Mathlib.Algebra.Group.InjSurj
Function.Surjective.addMonoid.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₂] [inst_1 : Zero M₂] [inst_2 : SMul ℕ M₂] [inst_3 : AddMonoid M₁]
  (f : M₁ → M₂) (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y)
  (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x),
  Function.Surjective.addMonoid f hf one mul npow =
    { toAddSemigroup := Function.Surjective.addSemigroup f hf mul,
      toZero := (Function.Surjective.addZeroClass f hf one mul).toZero, zero_add := ⋯, add_zero := ⋯,
      nsmul := fun n x => n • x, nsmul_zero := ⋯, nsmul_succ := ⋯ }
-- Init.Data.List.Basic
List.map_nil : ∀ {α : Type u} {β : Type v} {f : α → β}, List.map f [] = []
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey!_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → ∀ {km : α}, t.minKey! = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.instCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      CategoryTheory.Category.{max u₁ v, max (max (max (v + 1) u) u₁) v₁} (PresheafOfModules R)
-- Std.Async.Basic
Std.Async.EAsync.instForInLoopUnit : {ε : Type} → ForIn (Std.Async.EAsync ε) Lean.Loop Unit
-- Mathlib.Tactic.GCongr.Core
/-- (Internal for `gcongr`)
Elaborates to an expression satisfying `hasHoleAnnotation`.  -/
Mathlib.Tactic.GCongr.gcongrHoleExpand : Lean.ParserDescr
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
intEquivOfZMultiplesEqTop_symm_self : ∀ {G : Type u_2} [inst : Infinite G] [inst_1 : AddGroup G] (g : G) (hg : AddSubgroup.zmultiples g = ⊤),
  (intEquivOfZMultiplesEqTop g hg).symm g = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.cospanHomMk_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C}
  (z : F.obj CategoryTheory.Limits.WalkingCospan.one ⟶ G.obj CategoryTheory.Limits.WalkingCospan.one)
  (l : F.obj CategoryTheory.Limits.WalkingCospan.left ⟶ G.obj CategoryTheory.Limits.WalkingCospan.left)
  (r : F.obj CategoryTheory.Limits.WalkingCospan.right ⟶ G.obj CategoryTheory.Limits.WalkingCospan.right)
  (hl :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingCospan.Hom.inl) z =
        CategoryTheory.CategoryStruct.comp l (G.map CategoryTheory.Limits.WalkingCospan.Hom.inl))
      CategoryTheory.Limits.cospanHomMk._auto_1)
  (hr :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingCospan.Hom.inr) z =
        CategoryTheory.CategoryStruct.comp r (G.map CategoryTheory.Limits.WalkingCospan.Hom.inr))
      CategoryTheory.Limits.cospanHomMk._auto_3)
  (X : CategoryTheory.Limits.WalkingCospan),
  (CategoryTheory.Limits.cospanHomMk z l r hl hr).app X =
    Option.casesOn X z fun val => CategoryTheory.Limits.WalkingPair.casesOn val l r
-- Mathlib.Topology.Algebra.Valued.ValuedField
Valued.continuous_valuation : ∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [hv : Valued K Γ₀], Continuous ⇑Valued.v.restrict
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.finrank_rootSpanIn_int : ∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] {L : Type u_8}
  [inst_2 : Field L] [inst_3 : Module L M] [inst_4 : Module L N] (Q : RootPairing ι L M N) [Q.IsRootSystem] [Finite ι]
  [CharZero L] [Q.IsCrystallographic], Module.finrank ℤ ↥(Q.rootSpan ℤ) = Module.finrank L M
-- Init.Data.Dyadic.Basic
Dyadic.ble.eq_4 : ∀ (a a_1 : ℤ) (a_2 : a % 2 = 1) (b b_1 : ℤ) (b_2 : b % 2 = 1),
  (Dyadic.ofOdd a a_1 a_2).ble (Dyadic.ofOdd b b_1 b_2) =
    match b_1 - a_1 with
    | Int.ofNat l => decide (a <<< l ≤ b)
    | Int.negSucc l => decide (a ≤ b <<< (l + 1))
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.mk.inj : ∀ {R : Type u} {M : Type v} {inst : SMul R M} {carrier : Set M}
  {smul_mem' : ∀ (c : R) {x : M}, x ∈ carrier → c • x ∈ carrier} {carrier_1 : Set M}
  {smul_mem'_1 : ∀ (c : R) {x : M}, x ∈ carrier_1 → c • x ∈ carrier_1},
  { carrier := carrier, smul_mem' := smul_mem' } = { carrier := carrier_1, smul_mem' := smul_mem'_1 } →
    carrier = carrier_1
-- Mathlib.Topology.Algebra.ConstMulAction
AddAction.isOpenQuotientMap_quotientMk : ∀ {Γ : Type u_4} [inst : AddGroup Γ] {T : Type u_5} [inst_1 : TopologicalSpace T] [inst_2 : AddAction Γ T]
  [ContinuousConstVAdd Γ T], IsOpenQuotientMap (Quotient.mk (AddAction.orbitRel Γ T))
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.preimage_frontier : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set Y),
  ⇑h ⁻¹' frontier s = frontier (⇑h ⁻¹' s)
-- Batteries.Data.List.Lemmas
List.findIdxNth_cons_zero : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} {a : α},
  List.findIdxNth p (a :: xs) 0 = if p a = true then 0 else List.findIdxNth p xs 0 + 1
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.instIsIsoFunctorNatTrans : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {I : Type u_1}
  {F G : CategoryTheory.Functor (CategoryTheory.Discrete I) C} (f : (i : CategoryTheory.Discrete I) → F.obj i ⟶ G.obj i)
  [∀ (i : CategoryTheory.Discrete I), CategoryTheory.IsIso (f i)],
  CategoryTheory.IsIso (CategoryTheory.Discrete.natTrans f)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t₁.WF → t₂.WF → ∀ {k : α}, (t₁ ∩ t₂).getKey! k = if k ∈ t₂ then t₁.getKey! k else default
-- Mathlib.Order.LatticeIntervals
Set.Icc.lattice : {α : Type u_1} → {a b : α} → [inst : Lattice α] → Lattice ↑(Set.Icc a b)
-- Mathlib.Algebra.Order.Archimedean.Class
/-- Create a `FiniteArchimedeanClass` from a non-zero element.  -/
FiniteArchimedeanClass.mk : {M : Type u_1} →
  [inst : AddCommGroup M] →
    [inst_1 : LinearOrder M] → [inst_2 : IsOrderedAddMonoid M] → (a : M) → a ≠ 0 → FiniteArchimedeanClass M
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
SSet.S.cast.congr_simp : ∀ {X : SSet} (s s_1 : X.S) (e_s : s = s_1) {d d_1 : ℕ} (e_d : d = d_1) (hd : s.dim = d), s.cast hd = s_1.cast ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- A product over products is a product indexed by a product.  -/
CategoryTheory.Limits.Fan.IsLimit.prod : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type u_1} →
      {ι' : Type u_2} →
        {X : ι → ι' → C} →
          (c : (i : ι) → CategoryTheory.Limits.Fan fun j => X i j) →
            ((i : ι) → CategoryTheory.Limits.IsLimit (c i)) →
              (c' : CategoryTheory.Limits.Fan fun i => (c i).pt) →
                CategoryTheory.Limits.IsLimit c' →
                  CategoryTheory.Limits.IsLimit
                    (CategoryTheory.Limits.Fan.mk c'.pt fun p =>
                      CategoryTheory.CategoryStruct.comp (c'.proj p.1) ((c p.1).proj p.2))
-- Batteries.Data.String.Lemmas
String.get?_of_valid : ∀ (cs cs' : List Char), String.Pos.Raw.get? (String.ofList (cs ++ cs')) { byteIdx := String.utf8Len cs } = cs'.head?
-- Mathlib.Topology.Category.LightProfinite.Basic
/-- This is an auxiliary definition used to show that `LightDiagram` is essentially small.

Note that below we put a category instance on this structure which is completely different from the
category instance on `ℕᵒᵖ ⥤ FintypeCat.Skeleton.{u}`. Neither the morphisms nor the objects are the
same.
 -/
LightDiagram' : Type u
-- Mathlib.GroupTheory.GroupAction.Defs
/-- Decomposition of a type `X` as a disjoint union of its orbits under a group action.  -/
MulAction.selfEquivSigmaOrbits : (G : Type u_1) →
  (α : Type u_2) →
    [inst : Group G] →
      [inst_1 : MulAction G α] → α ≃ (ω : MulAction.orbitRel.Quotient G α) × ↑(MulAction.orbit G (Quotient.out ω))
-- Mathlib.Analysis.Convex.Cone.Closure
ConvexCone.coe_closure : ∀ {𝕜 : Type u_1} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] {E : Type u_2} [inst_2 : AddCommMonoid E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : SMul 𝕜 E] [inst_6 : ContinuousConstSMul 𝕜 E]
  (K : ConvexCone 𝕜 E), ↑K.closure = closure ↑K
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace_map : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y),
  AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace.map f = CategoryTheory.InducedCategory.homMk f.toHom
-- Mathlib.Probability.Independence.Process.Basic
/-- If `X` is a process independent from `Y` and for all `i`, `X' i` is almost everywhere equal
to `X i`, then `X'` is also independent from `Y`. This implies that independence results about
measurable processes should generally also hold
for processes whose marginals are only a.e.-measurable.  -/
ProbabilityTheory.IndepFun.process_congr_right : ∀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓧 : S → Type u_4} {𝓨 : Type u_5}
  [inst : (i : S) → MeasurableSpace (𝓧 i)] [inst_1 : MeasurableSpace 𝓨] {X X' : (i : S) → Ω → 𝓧 i} {Y : Ω → 𝓨},
  ProbabilityTheory.IndepFun Y (fun ω i => X i ω) P →
    (∀ (i : S), X i =ᵐ[P] X' i) → ProbabilityTheory.IndepFun Y (fun ω i => X' i ω) P
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
zero_cpow_eq_nhds : ∀ {b : ℂ}, b ≠ 0 → (fun x => 0 ^ x) =ᶠ[nhds b] 0
-- Mathlib.Data.Finset.Max
Finset.min_of_nonempty : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Finset α}, s.Nonempty → ∃ a, s.min = ↑a
-- Mathlib.Algebra.Order.Nonneg.Module
_private.Mathlib.Algebra.Order.Nonneg.Module.0.«termR≥0» : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
_private.Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm.0.mu_le : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R) {x y : R}
  (hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)) (n : ℕ),
  mu✝ μ hn n ≤ n
-- Mathlib.SetTheory.Cardinal.Order
/-- The **well-ordering theorem** (or **Zermelo's theorem**): every type can be well-ordered.  -/
exists_wellFoundedLT : ∀ (α : Type u), ∃ x, WellFoundedLT α
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.mapRingHom_comp_includeRight : ∀ {R : Type u_3} {S : Type u_4} {T : Type u_5} {R' : Type u_6} {S' : Type u_7} {T' : Type u_8} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : CommSemiring T] [inst_3 : Algebra R S] [inst_4 : Algebra R T]
  [inst_5 : CommSemiring R'] [inst_6 : CommSemiring S'] [inst_7 : CommSemiring T'] [inst_8 : Algebra R' S']
  [inst_9 : Algebra R' T'] (fR : R →+* R') (fS : S →+* S') (fT : T →+* T')
  (HS : fS.comp (algebraMap R S) = (algebraMap R' S').comp fR)
  (HT : fT.comp (algebraMap R T) = (algebraMap R' T').comp fR),
  (Algebra.TensorProduct.mapRingHom fR fS fT HS HT).comp ↑Algebra.TensorProduct.includeRight =
    (↑Algebra.TensorProduct.includeRight).comp fT
-- Std.Async.Select
/-- Attempts to retrieve a piece of data from the event source in a non-blocking fashion, returning
`some` if data is available and `none` otherwise.
 -/
Std.Async.Selector.tryFn : {α : Type} → Std.Async.Selector α → Std.Async.Async (Option α)
-- Mathlib.Algebra.Ring.AddAut
AddAut.mulLeft_apply_apply : ∀ {R : Type u_1} [inst : Semiring R] (x : Rˣ) (a : R), (AddAut.mulLeft x) a = x • a
-- Mathlib.Order.Interval.Finset.Basic
Finset.disjoint_Ioi_Iio : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] [inst_2 : LocallyFiniteOrderBot α] (a : α),
  Disjoint (Finset.Ioi a) (Finset.Iio a)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isNone_min?_eq_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp], t.WF → t.min?.isNone = t.isEmpty
-- Mathlib.Combinatorics.Quiver.Prefunctor
Prefunctor.mk.inj : ∀ {V : Type u₁} {inst : Quiver V} {W : Type u₂} {inst_1 : Quiver W} {obj : V → W}
  {map : {X Y : V} → (X ⟶ Y) → (obj X ⟶ obj Y)} {obj_1 : V → W} {map_1 : {X Y : V} → (X ⟶ Y) → (obj_1 X ⟶ obj_1 Y)},
  { obj := obj, map := map } = { obj := obj_1, map := map_1 } → obj = obj_1 ∧ map ≍ map_1
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.neg_subset : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {s t : Set α}, -s ⊆ t ↔ s ⊆ -t
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.const_fac_thru_zero : ∀ (n m : SimplexCategory) (i : Fin (m.len + 1)),
  n.const m i = CategoryTheory.CategoryStruct.comp (n.const { len := 0 } 0) ({ len := 0 }.const m i)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.instInhabitedExpr.default : Lean.Grind.Linarith.Expr
-- Mathlib.Data.PFunctor.Multivariate.W
/-- **Alias** of `MvPFunctor.wpInd`.

---

Induction principle for an unfolded `W`  -/
MvPFunctor.wp_ind : {n : ℕ} →
  (P : MvPFunctor.{u} (n + 1)) →
    {α : TypeVec.{u_1} n} →
      {C : (x : P.last.W) → TypeVec.Arrow (P.WPath x) α → Sort v} →
        ((a : P.A) →
            (f : P.last.B a → P.last.W) →
              (f' : TypeVec.Arrow (P.WPath (WType.mk a f)) α) →
                ((i : P.last.B a) → C (f i) (P.wPathDestRight f' i)) → C (WType.mk a f) f') →
          (x : P.last.W) → (f' : TypeVec.Arrow (P.WPath x) α) → C x f'
-- Init.Data.Dyadic.Basic
_private.Init.Data.Dyadic.Basic.0.Dyadic.toRat.match_1.eq_1 : ∀ (motive : Dyadic → Sort u_1) (h_1 : Unit → motive Dyadic.zero)
  (h_2 : (n : ℤ) → (k : ℕ) → (hn : n % 2 = 1) → motive (Dyadic.ofOdd n (Int.ofNat k) hn))
  (h_3 : (n : ℤ) → (k : ℕ) → (hn : n % 2 = 1) → motive (Dyadic.ofOdd n (Int.negSucc k) hn)),
  (match Dyadic.zero with
    | Dyadic.zero => h_1 ()
    | Dyadic.ofOdd n (Int.ofNat k) hn => h_2 n k hn
    | Dyadic.ofOdd n (Int.negSucc k) hn => h_3 n k hn) =
    h_1 ()
-- Mathlib.Data.NNReal.Defs
NNReal.instOne : One NNReal
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.dist_coe_center : ∀ (z w : UpperHalfPlane) (r : ℝ),
  dist ↑z ↑(w.center r) = √(2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2)
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.GrowsPolynomially.add : ∀ {f g : ℝ → ℝ},
  AkraBazziRecurrence.GrowsPolynomially f →
    AkraBazziRecurrence.GrowsPolynomially g →
      0 ≤ᶠ[Filter.atTop] f → 0 ≤ᶠ[Filter.atTop] g → AkraBazziRecurrence.GrowsPolynomially fun x => f x + g x
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.L1.hasFiniteIntegral_coeFn : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  (f : ↥(MeasureTheory.Lp β 1 μ)), MeasureTheory.HasFiniteIntegral (↑↑f) μ
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
PresheafOfModules.braiding_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat}
  (M₁ M₂ : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))) (X : Cᵒᵖ),
  (β_ M₁ M₂).hom.app X = (β_ (M₁.obj X) (M₂.obj X)).hom
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.instantiateMVarsAtHeader : Lean.Elab.DefViewElabHeader → Lean.Elab.TermElabM Lean.Elab.DefViewElabHeader
-- Mathlib.LinearAlgebra.Matrix.Echelon.Pivot
Matrix.IsPivotedBy.isRowEchelon : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Zero R] [inst_1 : LT m] [inst_2 : LT n] {A : Matrix m n R}
  {l : m → WithTop n}, A.IsPivotedBy l → A.IsRowEchelon
-- Init.Data.UInt.Lemmas
UInt64.mul_two : ∀ {a : UInt64}, a * 2 = a + a
-- Batteries.Control.Lemmas
StateT.run_tryCatchThe : ∀ {m : Type u_1 → Type u_2} {ε : Type u_3} {σ α : Type u_1} [inst : Monad m] [inst_1 : MonadExceptOf ε m]
  (body : StateT σ m α) (handler : ε → StateT σ m α) (s : σ),
  (tryCatchThe ε body handler).run s = tryCatchThe ε (body.run s) fun x => (handler x).run s
-- Mathlib.Algebra.Group.End
AddAutAdditive_symm_apply_apply : ∀ (G : Type u_3) [inst : Group G] (a : G ≃* G) (a_1 : Additive G),
  ((AddAutAdditive G).symm a) a_1 = Additive.ofMul (a (Additive.toMul a_1))
-- Mathlib.Order.Monotone.Basic
StrictAnti.isMax_of_apply : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {a : α},
  StrictAnti f → IsMin (f a) → IsMax a
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.Position.line : Lean.Lsp.Position → ℕ
-- Mathlib.Order.Heyting.Basic
himp_idem : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b : α}, b ⇨ b ⇨ a = b ⇨ a
-- Mathlib.Computability.TuringMachine.Computable
Turing.TM2Computable.mk.inj : ∀ {α β αΓ βΓ : Type} {ea : α → List αΓ} {eb : β → List βΓ} {f : α → β}
  {toTM2ComputableAux : Turing.TM2ComputableAux αΓ βΓ}
  {outputsFun :
    (a : α) →
      Turing.TM2Outputs toTM2ComputableAux.tm (List.map toTM2ComputableAux.inputAlphabet.invFun (ea a))
        (some (List.map toTM2ComputableAux.outputAlphabet.invFun (eb (f a))))}
  {toTM2ComputableAux_1 : Turing.TM2ComputableAux αΓ βΓ}
  {outputsFun_1 :
    (a : α) →
      Turing.TM2Outputs toTM2ComputableAux_1.tm (List.map toTM2ComputableAux_1.inputAlphabet.invFun (ea a))
        (some (List.map toTM2ComputableAux_1.outputAlphabet.invFun (eb (f a))))},
  { toTM2ComputableAux := toTM2ComputableAux, outputsFun := outputsFun } =
      { toTM2ComputableAux := toTM2ComputableAux_1, outputsFun := outputsFun_1 } →
    toTM2ComputableAux = toTM2ComputableAux_1 ∧ outputsFun ≍ outputsFun_1
-- Std.Http.Data.Headers.Basic
Std.Http.Header.instBEqContentLength.beq : Std.Http.Header.ContentLength → Std.Http.Header.ContentLength → Bool
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.pow_apply_eq_self_of_apply_eq_self : ∀ {α : Type u_1} {f : Equiv.Perm α} {x : α}, f x = x → ∀ (n : ℕ), (f ^ n) x = x
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.toLinearMap₂'_toMatrix' : ∀ {R : Type u_1} {S₁ : Type u_3} {S₂ : Type u_5} {N₂ : Type u_10} {n : Type u_11} {m : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid N₂] [inst_2 : Module R N₂] [inst_3 : Semiring S₁]
  [inst_4 : Semiring S₂] [inst_5 : Module S₁ N₂] [inst_6 : Module S₂ N₂] [inst_7 : SMulCommClass S₁ R N₂]
  [inst_8 : SMulCommClass S₂ R N₂] [inst_9 : SMulCommClass S₂ S₁ N₂] [inst_10 : Fintype n] [inst_11 : Fintype m]
  [inst_12 : DecidableEq n] [inst_13 : DecidableEq m] (B : (n → S₁) →ₗ[S₁] (m → S₂) →ₗ[S₂] N₂),
  (Matrix.toLinearMap₂' R) ((LinearMap.toMatrix₂' R) B) = B
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.one_smul : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_2}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (f : M →ₚₗ[R] N), 1 • f = f
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.zipWith.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : List α → List β → Sort u_3) →
      (x : List α) →
        (x_1 : List β) →
          ((x : α) → (xs : List α) → (y : β) → (ys : List β) → motive (x :: xs) (y :: ys)) →
            ((x : List α) →
                (x_2 : List β) →
                  (∀ (x_3 : α) (xs : List α) (y : β) (ys : List β), x = x_3 :: xs → x_2 = y :: ys → False) →
                    motive x x_2) →
              motive x x_1
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.scaleRoots_eval₂_eq_zero_of_eval₂_div_eq_zero : ∀ {S : Type u_2} {K : Type u_4} [inst : Semiring S] [inst_1 : Field K] {p : Polynomial S} {f : S →+* K},
  Function.Injective ⇑f →
    ∀ {r s : S},
      Polynomial.eval₂ f (f r / f s) p = 0 → s ∈ nonZeroDivisors S → Polynomial.eval₂ f (f r) (p.scaleRoots s) = 0
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.neg_snd : ∀ {q : ℕ} (x : LucasLehmer.X q), (-x).2 = -x.2
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPAll : Lean.Options → Bool
-- Mathlib.Combinatorics.Matroid.Closure
/-- **Alias** of `Matroid.indep_iff_forall_closure_sdiff_ne`. -/
Matroid.indep_iff_forall_closure_diff_ne : ∀ {α : Type u_2} {M : Matroid α} {I : Set α}, M.Indep I ↔ ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
-- Mathlib.Order.Interval.Finset.Basic
Finset.card_Ioo_eq_card_Ico_sub_one : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] (a b : α),
  (Finset.Ioo a b).card = (Finset.Ico a b).card - 1
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.offset_of_isLongestMatchAt : ∀ {pat s : String.Slice} {pos₁ pos₂ : s.Pos},
  pat.isEmpty = false →
    String.Slice.Pattern.Model.IsLongestMatchAt pat pos₁ pos₂ → pos₂.offset = pos₁.offset.increaseBy pat.utf8ByteSize
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.Code.sizeLe.inc : ℕ → EStateM Unit ℕ Unit
-- Mathlib.Order.Filter.Prod
Filter.coprod_eq_prod_top_sup_top_prod : ∀ {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter β), f.coprod g = f ×ˢ ⊤ ⊔ ⊤ ×ˢ g
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.forIn'.loop.match_3.eq_1 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.done b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_1 b
-- Mathlib.LinearAlgebra.Dual.Basis
Module.DualBases.basis_repr_apply : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {e : ι → M} {ε : ι → Module.Dual R M} (h : Module.DualBases e ε) (m : M), h.basis.repr m = h.coeffs m