mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
CategoryTheory.Free.lift_additive : ∀ (R : Type u_1) [inst : CommRing R] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] {D : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} D] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.Linear R D] (F : CategoryTheory.Functor C D), (CategoryTheory.Free.lift R F).Additive
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearMap.BilinForm.compLeft_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (B : LinearMap.BilinForm R M) (f : M →ₗ[R] M) (v w : M), ((B.compLeft f) v) w = (B (f v)) w
-- Mathlib.Data.Fin.Tuple.Basic
Fin.range_snoc : ∀ {n : ℕ} {α : Type u_2} (f : Fin n → α) (x : α), Set.range (Fin.snoc f x) = insert x (Set.range f)
-- Mathlib.Topology.Order.Basic
Function.invFunOn.congr_simp : ∀ {α : Type u_1} {β : Type u_2} [inst : Nonempty α] (f f_1 : α → β),
  f = f_1 →
    ∀ (s s_1 : Set α), s = s_1 → ∀ (b b_1 : β), b = b_1 → Function.invFunOn f s b = Function.invFunOn f_1 s_1 b_1
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.yonedaEquiv_symm_app_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
  (x : F.obj (Opposite.op X)) (Y : Cᵒᵖ) (f : Opposite.unop Y ⟶ X),
  (CategoryTheory.ConcreteCategory.hom (F.map f.op)) x = (CategoryTheory.ConcreteCategory.hom (F.map f.op)) x
-- Init.Data.Int.Basic
IntCast.mk : {R : Type u} → (ℤ → R) → IntCast R
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObjCat.forget₂Mon_map_hom : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y : CategoryTheory.RingObjCat C} (f : X ⟶ Y),
  ((CategoryTheory.RingObjCat.forget₂Mon C).map f).hom = f.hom
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.leadingCoeff_preΨ' : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) {n : ℕ},
  ↑n ≠ 0 → (W.preΨ' n).leadingCoeff = ↑(if Even n then n / 2 else n)
-- Mathlib.Data.Finset.SDiff
Finset.sdiff_inter_distrib_right : ∀ {α : Type u_1} [inst : DecidableEq α] (s t u : Finset α), s \ (t ∩ u) = s \ t ∪ s \ u
-- Mathlib.LinearAlgebra.Isomorphisms
Submodule.quotientQuotientEquivQuotientAux.congr_simp : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (S T : Submodule R M)
  (h : S ≤ T), S.quotientQuotientEquivQuotientAux T h = S.quotientQuotientEquivQuotientAux T h
-- Batteries.Data.BinomialHeap.Basic
/-- `O(n)`. Fold a monadic function over the tree structure to accumulate a value.  -/
Batteries.BinomialHeap.Imp.Heap.foldTreeM : {m : Type u_1 → Type u_2} →
  {β : Type u_1} → {α : Type u_3} → [Monad m] → β → (α → β → β → m β) → Batteries.BinomialHeap.Imp.Heap α → m β
-- Mathlib.Algebra.QuadraticAlgebra.Basic
/-- **Alias** of the forward direction of `QuadraticAlgebra.norm_eq_one_iff_mem_unitary`.

---

An element of `QuadraticAlgebra R a b` has norm equal to `1`
if and only if it is contained in the submonoid of unitary elements.  -/
QuadraticAlgebra.mem_unitary : ∀ {R : Type u_2} {a b : R} [inst : CommRing R] {z : QuadraticAlgebra R a b},
  QuadraticAlgebra.norm z = 1 → z ∈ unitary (QuadraticAlgebra R a b)
-- Init.Data.Array.Lemmas
Array.isEmpty_iff_size_eq_zero : ∀ {α : Type u_1} {xs : Array α}, xs.isEmpty = true ↔ xs.size = 0
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_im_ax : ∀ {K : semiOutParam (Type u_1)} [self : RCLike K] (r : ℝ), RCLike.im ((algebraMap ℝ K) r) = 0
-- Lean.Elab.ConfigEval.Basic
Lean.Elab.ConfigEval.EvalTerm.evalTermWithInfo : {α : Type} →
  Option Lean.Expr → (Lean.Term → Lean.Elab.TermElabM (α × Lean.Expr)) → Lean.Term → Lean.Elab.TermElabM (α × Lean.Expr)
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instVAdd' : {β : Type u_2} → {α : Type u_1} → [VAdd β α] → VAdd (Colex β) α
-- Mathlib.Computability.Primrec.List
Primrec.list_casesOn : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α → List β} {g : α → σ} {h : α → β × List β → σ},
  Primrec f → Primrec g → Primrec₂ h → Primrec fun a => List.casesOn (f a) (g a) fun b l => h a (b, l)
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPCoercionsTypes : Lean.Options → Bool
-- Init.Data.List.Sublist
List.prefix_refl : ∀ {α : Type u_1} (l : List α), l <+: l
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.codisjoint_map : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [inst_3 : MonoidHomClass F M N] {f : F},
  Function.Surjective ⇑f → ∀ {H K : Submonoid M}, Codisjoint H K → Codisjoint (Submonoid.map f H) (Submonoid.map f K)
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.mem_carrier : ∀ {M : Type u_1} [inst : Add M] {s : AddSubsemigroup M} {x : M}, x ∈ s.carrier ↔ x ∈ s
-- Init.Grind.Module.Basic
/-- Scalar multiplication by a successor.  -/
Lean.Grind.NatModule.add_one_nsmul : ∀ {M : Type u} [self : Lean.Grind.NatModule M] (n : ℕ) (a : M), (n + 1) • a = n • a + a
-- Mathlib.Tactic.Simproc.ExistsAndEq
/-- When `P = ∃ f₁ ... fₙ, body`, where `exs = [f₁, ..., fₙ]`, this function takes
`act : body → goal` and proves `P → goal` using `Exists.elim`.

Example:
```
exs = []: act h
exs = [b]:
  P := ∃ b, body
  Exists.elim h (fun b hb ↦ act hb)
exs = [b, c]:
  P := ∃ b c, body
  Exists.elim h (fun b hb ↦
    Exists.elim hb (fun c hc ↦ act hc)
  )
...
```  -/
ExistsAndEq.withNestedExistsElim : {P body goal : Q(Prop)} → List ExistsAndEq.VarQ → Q(«$P») → (Q(«$body») → Lean.MetaM Q(«$goal»)) → Lean.MetaM Q(«$goal»)
-- Init.Data.BitVec.Lemmas
BitVec.setWidth_mul : ∀ {w i : ℕ} (x y : BitVec w), i ≤ w → BitVec.setWidth i (x * y) = BitVec.setWidth i x * BitVec.setWidth i y
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.IsSymmetric.pow : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E}, T.IsSymmetric → ∀ (n : ℕ), (T ^ n).IsSymmetric
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.ae_bdd_liminf_atTop_of_eLpNorm_bdd : ∀ {α : Type u_1} {E : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : MeasurableSpace E] [OpensMeasurableSpace E] {R : NNReal} {p : ENNReal},
  p ≠ 0 →
    ∀ {f : ℕ → α → E},
      (∀ (n : ℕ), Measurable (f n)) →
        (∀ (n : ℕ), MeasureTheory.eLpNorm (f n) p μ ≤ ↑R) →
          ∀ᵐ (x : α) ∂μ, Filter.liminf (fun n => ‖f n x‖ₑ) Filter.atTop < ⊤
-- Mathlib.Algebra.Category.Grp.Basic
/-- An alias for `AddGrpCat.{max u v}`, to deal around unification issues.  -/
AddGrpMax : Type ((max u1 u2) + 1)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.GeneratingSections.opEpi_comp : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {M N P : SheafOfModules R} (σ : M.GeneratingSections) (p : M ⟶ N)
  (q : N ⟶ P) [inst_3 : CategoryTheory.Epi p] [inst_4 : CategoryTheory.Epi q],
  σ.ofEpi (CategoryTheory.CategoryStruct.comp p q) = (σ.ofEpi p).ofEpi q
-- Mathlib.Data.Nat.Find
/-- A weak version of `Nat.find_congr`, requiring `p = q` everywhere.  -/
Nat.find_congr' : ∀ {p q : ℕ → Prop} [inst : DecidablePred p] [inst_1 : DecidablePred q] {hp : ∃ n, p n} {hq : ∃ n, q n},
  (∀ {n : ℕ}, p n ↔ q n) → Nat.find hp = Nat.find hq
-- Mathlib.Tactic.DeclarationNames
/-- If `pos` is a `String.Pos`, then `getNamesFrom pos` returns the array of identifiers
for the names of the declarations whose syntax begins in position at least `pos`.
 -/
Mathlib.Linter.getNamesFrom : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → [Lean.MonadFileMap m] → String.Pos.Raw → m (Array Lean.Syntax)
-- Mathlib.NumberTheory.Divisors
/-- Pairs of divisors of a natural number, as a list.

`n.divisorsAntidiagonalList` is the list of pairs `(a, b) : ℕ × ℕ` such that `a * b = n`, ordered
by increasing `a`. By convention, we set `Nat.divisorsAntidiagonalList 0 = []`.
 -/
Nat.divisorsAntidiagonalList : ℕ → List (ℕ × ℕ)
-- Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
MeasureTheory.integral_sum_measure : ∀ {ι : Type u_1} {X : Type u_2} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  {μ : ι → MeasureTheory.Measure X} {f : X → E} [inst_1 : NormedSpace ℝ E],
  MeasureTheory.Integrable f (MeasureTheory.Measure.sum μ) →
    ∫ (x : X), f x ∂MeasureTheory.Measure.sum μ = ∑' (i : ι), ∫ (x : X), f x ∂μ i
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.comp_snd : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
  {l : Filter α} (l' : Filter β), f =Θ[l] g → (f ∘ Prod.snd) =Θ[l' ×ˢ l] (g ∘ Prod.snd)
-- Init.Data.UInt.Bitwise
USize.and_neg_one : ∀ {a : USize}, a &&& -1 = a
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.cardSupp_one : ∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : Zero Γ] [inst_3 : One R] [NeZero 1],
  HahnSeries.cardSupp 1 = 1
-- Mathlib.Data.Set.Lattice.Image
Set.iInter_iInter_eq' : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : ι → α} {g : α → Set β},
  ⋂ x, ⋂ y, ⋂ (_ : f y = x), g x = ⋂ y, g (f y)
-- Init.Data.SInt.Lemmas
ISize.toInt_toInt8 : ∀ (x : ISize), x.toInt8.toInt = x.toInt.bmod (2 ^ 8)
-- Mathlib.Algebra.Lie.Basic
zsmul_lie : ∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] (x : L) (m : M)
  (a : ℤ), ⁅a • x, m⁆ = a • ⁅x, m⁆
-- Mathlib.Data.Set.Basic
Set.eq_univ_iff_forall : ∀ {α : Type u} {s : Set α}, s = Set.univ ↔ ∀ (x : α), x ∈ s
-- Init.Data.Nat.Simproc
Nat.Simproc.sub_add_eq_comm : ∀ (a b c : ℕ), a - (b + c) = a - c - b
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.skipPrefix? : String.Slice → (s : String.Slice) → Option s.Pos
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.Iff.realize_bd_iff : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {M : Type u_1} [Nonempty M] [inst : L.Structure M]
  [M ⊨ T] {φ ψ : L.BoundedFormula α n}, T.Iff φ ψ → ∀ {v : α → M} {xs : Fin n → M}, φ.Realize v xs ↔ ψ.Realize v xs
-- Mathlib.Data.EReal.Basic
EReal.coe_ennreal_toReal : ∀ {x : ENNReal}, x ≠ ⊤ → ↑x.toReal = ↑x
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.toEquiv_mulRight₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : MeasurableSpace G₀] [inst_2 : MeasurableMul G₀] {g : G₀}
  (hg : g ≠ 0), (MeasurableEquiv.mulRight₀ g hg).toEquiv = Equiv.mulRight₀ g hg
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
/-- An element of a product algebra is integral if each component is integral.  -/
IsIntegral.pair : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Ring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {x : A × B}, IsIntegral R x.1 → IsIntegral R x.2 → IsIntegral R x
-- Mathlib.Topology.MetricSpace.IsometricSMul
nndist_div_left : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G]
  (a b c : G), nndist (a / b) (a / c) = nndist b c
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- `SimpleFunc.lintegral` is monotone both in function and in measure.  -/
MeasureTheory.SimpleFunc.lintegral_mono : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {f g : MeasureTheory.SimpleFunc α ENNReal},
  f ≤ g → μ ≤ ν → f.lintegral μ ≤ g.lintegral ν
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Complex.not_differentiableAt_Gamma_zero : ¬DifferentiableAt ℂ Complex.Gamma 0
-- Mathlib.Analysis.PSeries
/-- Cauchy condensation test for antitone series of nonnegative real numbers.  -/
summable_condensed_iff_of_nonneg : ∀ {f : ℕ → ℝ},
  (∀ (n : ℕ), 0 ≤ f n) → (∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m) → ((Summable fun k => 2 ^ k * f (2 ^ k)) ↔ Summable f)
-- Mathlib.SetTheory.Cardinal.Basic
/-- See also `Cardinal.nsmul_lt_aleph0_iff_of_ne_zero` if you already have `n ≠ 0`.  -/
Cardinal.nsmul_lt_aleph0_iff : ∀ {a : Cardinal.{u_1}} {n : ℕ}, n • a < Cardinal.aleph0 ↔ n = 0 ∨ a < Cardinal.aleph0
-- Init.Data.LawfulHashable
/-- If `a == b`, then `hash a = hash b`.  -/
LawfulHashable.hash_eq : ∀ {α : Type u} {inst : BEq α} {inst_1 : Hashable α} [self : LawfulHashable α] (a b : α),
  (a == b) = true → hash a = hash b
-- Init.Prelude
/-- Non-strict, or weak, inequality of natural numbers, usually accessed via the `≤` operator.
 -/
Nat.le : ℕ → ℕ → Prop
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
/-- The support of an ideal sheaf. Also see `IdealSheafData.mem_support_iff_of_mem`.  -/
AlgebraicGeometry.Scheme.IdealSheafData.support : {X : AlgebraicGeometry.Scheme} → X.IdealSheafData → TopologicalSpace.Closeds ↥X
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.LeftExtension.precomp_obj_right : ∀ {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C'] [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H)
  (G : CategoryTheory.Functor C' C)
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D H).obj L)),
  ((CategoryTheory.Functor.LeftExtension.precomp L F G).obj X).right = X.right
-- Lean.Meta.Sym.Arith.Poly
_private.Lean.Meta.Sym.Arith.Poly.0.Lean.Grind.CommRing.Mon.toExpr.go : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.equiv_apply : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] (self : E →SWOT[σ] F),
  ContinuousLinearMapWOT.equiv self = self.toCLM
-- Init.Data.BitVec.Bitblast
/-- Heuristically, `y <<< x` is much larger than `x`,
and hence low bits of `y <<< x`. Thus, `x + (y <<< x) = x ||| (y <<< x).`  -/
BitVec.add_shiftLeft_eq_or_shiftLeft : ∀ {w : ℕ} {x y : BitVec w}, x + y <<< x = x ||| y <<< x
-- Std.Data.HashSet.Lemmas
Std.HashSet.mem_insert_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  k ∈ m.insert k
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
Std.IterM.toArray_uLift : ∀ {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} [inst : Std.Iterator α m β]
  [inst_1 : Monad m] [inst_2 : Monad n] {it : Std.IterM m β} [inst_3 : MonadLiftT m (Std.Iterators.ULiftT n)]
  [Std.Iterators.Finite α m] [LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m (Std.Iterators.ULiftT n)],
  (it.uLift n).toArray = (fun l => Array.map ULift.up l.down) <$> (monadLift it.toArray).run
-- Lean.Elab.Command
Lean.Elab.Command.Context.currMacroScope : Lean.Elab.Command.Context → Lean.MacroScope
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- Constructor for `ReflexiveCofork`  -/
CategoryTheory.Limits.ReflexiveCofork.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C} →
      {X : C} →
        (π : F.obj CategoryTheory.Limits.WalkingReflexivePair.zero ⟶ X) →
          CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left) π =
              CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right) π →
            CategoryTheory.Limits.ReflexiveCofork F
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.RealizeConstResult.mk : Lean.VisibilityMap✝ (List Lean.AsyncConst✝) →
  (Lean.Kernel.Environment → Task (Except Lean.Kernel.Exception Lean.Kernel.Environment)) →
    Dynamic → Lean.Environment.RealizeConstResult✝
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.mem_range_self : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (x : M), f x ∈ f.range
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.size : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Zipper α β → ℕ
-- Mathlib.Analysis.Calculus.ContDiff.Operations
contDiff_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type uF} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {𝕜' : Type u_3} [inst_3 : NormedRing 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  [inst_5 : Module 𝕜' F] [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F], ContDiff 𝕜 n fun p => p.1 • p.2
-- Mathlib.Data.Finset.Fold
/-- A weaker version of `Finset.fold_ite'`,
relying on typeclass idempotency over the whole type,
instead of solely on the seed element.
However, this is easier to use because it does not generate side goals.  -/
Finset.fold_ite : ∀ {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β} {b : β}
  {s : Finset α} [Std.IdempotentOp op] {g : α → β} (p : α → Prop) [inst : DecidablePred p],
  Finset.fold op b (fun i => if p i then f i else g i) s =
    op (Finset.fold op b f (Finset.filter p s)) (Finset.fold op b g ({i ∈ s | ¬p i}))
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instVAddAssocClass : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : VAdd M X] [inst_2 : ContinuousConstVAdd M X]
  {N : Type u_3} [inst_3 : VAdd N X] [inst_4 : VAdd M N] [inst_5 : ContinuousConstVAdd N X] [VAddAssocClass M N X],
  VAddAssocClass M N (SeparationQuotient X)
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.categoryFormatterCore : Lean.Name → Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.mk.inj : ∀ {V : Type u_1} {W : Type u_2} {inst : SeminormedAddCommGroup V} {inst_1 : SeminormedAddCommGroup W} {toFun : V → W}
  {map_add' : ∀ (v₁ v₂ : V), toFun (v₁ + v₂) = toFun v₁ + toFun v₂} {bound' : ∃ C, ∀ (v : V), ‖toFun v‖ ≤ C * ‖v‖}
  {toFun_1 : V → W} {map_add'_1 : ∀ (v₁ v₂ : V), toFun_1 (v₁ + v₂) = toFun_1 v₁ + toFun_1 v₂}
  {bound'_1 : ∃ C, ∀ (v : V), ‖toFun_1 v‖ ≤ C * ‖v‖},
  { toFun := toFun, map_add' := map_add', bound' := bound' } =
      { toFun := toFun_1, map_add' := map_add'_1, bound' := bound'_1 } →
    toFun = toFun_1
-- Mathlib.Data.NNRat.Defs
NNRat.coe_injective : Function.Injective NNRat.cast
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
Complex.iter_deriv_exp : ∀ (n : ℕ), deriv^[n] Complex.exp = Complex.exp
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.vadd_univ : ∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddAction α β] {s : Set α},
  s.Nonempty → s +ᵥ Set.univ = Set.univ
-- Mathlib.Data.Sum.Order
Sum.instIsTransLex : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [IsTrans α r] [IsTrans β s],
  IsTrans (α ⊕ β) (Sum.Lex r s)
-- Lean.Meta.Tactic.Grind.Main
_private.Lean.Meta.Tactic.Grind.Main.0.Lean.Meta.Grind.mkCleanState : Lean.MVarId → Lean.Meta.Grind.GrindM Lean.Meta.Grind.Clean.State
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.encodeCode.eq_1 : Nat.Partrec.Code.zero.encodeCode = 0
-- Lean.Environment
Lean.Kernel.Exception.declHasMVars : Lean.Kernel.Environment → Lean.Name → Lean.Expr → Lean.Kernel.Exception
-- Init.Data.Fin.Fold
Fin.foldr_add : ∀ {n m : ℕ} {α : Sort u_1} (f : Fin (n + m) → α → α) (x : α),
  Fin.foldr (n + m) f x = Fin.foldr n (fun i => f (Fin.castLE ⋯ i)) (Fin.foldr m (fun i => f (Fin.natAdd n i)) x)
-- Mathlib.Topology.Instances.Complex
/-- The only closed subfields of `ℂ` are `ℝ` and `ℂ`.  -/
Complex.subfield_eq_of_closed : ∀ {K : Subfield ℂ}, IsClosed ↑K → K = Complex.ofRealHom.fieldRange ∨ K = ⊤
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
range_cfcₙ_nnreal : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : Module ℝ A] [inst_3 : IsScalarTower ℝ A A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : TopologicalSpace A] [inst_6 : IsTopologicalRing A] [T2Space A]
  [inst_8 : PartialOrder A] [inst_9 : NonnegSpectrumClass ℝ A] [inst_10 : StarOrderedRing A] [inst_11 : StarModule ℝ A]
  [inst_12 : ContinuousStar A] [inst_13 : ContinuousConstSMul ℝ A]
  [inst_14 : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A),
  autoParam (0 ≤ a) range_cfcₙ_nnreal._auto_1 →
    (Set.range fun x => cfcₙ x a) = {x | x ∈ NonUnitalStarAlgebra.elemental ℝ a ∧ 0 ≤ x}
-- Mathlib.RepresentationTheory.Homological.ContCohomology.LowDegree
ContinuousCohomology.cocycles₀IsoAux' : ∀ {k : Type u_1} {G : Type u_2} [inst : Ring k] [inst_1 : Group G] [inst_2 : TopologicalSpace k]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] (X : TopRep k G) (x : ↑X)
  (h : ContinuousMap.const G x ∈ (X.resolution'.X 0).ρ.invariants),
  ⟨ContinuousMap.const G x, h⟩ ∈ (↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker
-- Lean.Parser.Syntax
Lean.Parser.Command.mixfix.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- The replacement expression obtained from the rewrite  -/
Mathlib.Tactic.LibraryRewrite.RewriteInterface.replacement : Mathlib.Tactic.LibraryRewrite.RewriteInterface → Lean.Expr
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.map_id : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictlyUnitaryPseudofunctor B C) (X : B),
  self.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (self.obj X)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftIso_counitIso_hom_app_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ : CategoryTheory.Functor A T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : L₁ ≅ L₂) (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftIso R e).counitIso.hom.app X).right =
    CategoryTheory.CategoryStruct.id X.right
-- Init.Data.UInt.Bitwise
UInt64.toUInt16_xor : ∀ (a b : UInt64), (a ^^^ b).toUInt16 = a.toUInt16 ^^^ b.toUInt16
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.root'In_corootSpanMem_eq_pairingIn : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i j : ι)
  (S : Type u_6) [inst_5 : CommRing S] [inst_6 : Algebra S R] [inst_7 : Module S N] [inst_8 : IsScalarTower S R N]
  [inst_9 : FaithfulSMul S R] [inst_10 : P.IsValuedIn S], (P.root'In S i) (P.corootSpanMem S j) = P.pairingIn S i j
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_map_equiv : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} {s : Finset ι} [inst : CommMonoid M] {f : ι → M} (e : ι ≃ κ),
  (Finset.map e.toEmbedding s).prod (f ∘ ⇑e.symm) = s.prod f
-- Mathlib.Data.Set.Pairwise.Basic
/-- The partial images of a binary function `f` whose partial evaluations are injective are pairwise
disjoint iff `f` is injective .  -/
Set.pairwiseDisjoint_image_right_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {s : Set α} {t : Set β},
  (∀ a ∈ s, Function.Injective (f a)) →
    ((s.PairwiseDisjoint fun a => f a '' t) ↔ Set.InjOn (fun p => f p.1 p.2) (s ×ˢ t))
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.instPow : Pow ℝ ℝ