mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
/-- In cartesian monoidal categories, any morphism to the terminal tensor unit has a functorial
choice of pullbacks.  -/
CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {X : C} → (f : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) → CategoryTheory.ChosenPullbacksAlong f
-- Mathlib.Order.FixedPoints
OrderHom.nextFixed_le_iff : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} (hx : x ≤ f x) {y : ↑(Function.fixedPoints ⇑f)},
  f.nextFixed x hx ≤ y ↔ x ≤ ↑y
-- Mathlib.Data.Complex.Basic
Complex.I_ne_zero : Complex.I ≠ 0
-- Mathlib.Analysis.ODE.Transform
IsIntegralCurveAt.comp_mul_ne_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {t₀ : ℝ},
  IsIntegralCurveAt γ v t₀ → ∀ {a : ℝ}, a ≠ 0 → IsIntegralCurveAt (γ ∘ fun x => x * a) (a • v ∘ fun x => x * a) (t₀ / a)
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.tail.sizeOf_spec : sizeOf Turing.ToPartrec.Code.tail = 1
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
/-- The right unitor isomorphism for the monoidal structure in `AugmentedSimplexCategory`  -/
AugmentedSimplexCategory.rightUnitor : (x : AugmentedSimplexCategory) → x.tensorObj AugmentedSimplexCategory.tensorUnit ≅ x
-- Mathlib.NumberTheory.Padics.RingHoms
_private.Mathlib.NumberTheory.Padics.RingHoms.0.PadicInt.appr.match_1.eq_2 : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (motive : ℤ_[p] → ℕ → Sort u_1) (x : ℤ_[p]) (n : ℕ)
  (h_1 : (_x : ℤ_[p]) → motive _x 0) (h_2 : (x : ℤ_[p]) → (n : ℕ) → motive x n.succ),
  (match x, n.succ with
    | _x, 0 => h_1 _x
    | x, n.succ => h_2 x n) =
    h_2 x n
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Auxiliary type for the `checkCoverage` function.
 -/
Lean.Meta.Grind.CheckCoverageResult : Type
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₄'_inv_hom_id : ∀ {C : Type u_1} {ι' : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : Preorder ι'] (X' : CategoryTheory.Abelian.SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁)
  (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ)
  (h : CategoryTheory.Limits.IsZero ((X'.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hi₃₄))))
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₄'_inv_hom_id._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.isoMapFourδ₄Toδ₄'_inv_hom_id._auto_3),
  CategoryTheory.CategoryStruct.comp (X'.isoMapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂).inv
      (X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂) =
    CategoryTheory.CategoryStruct.id
      (X'.E (CategoryTheory.homOfLE hi₀₁) (CategoryTheory.homOfLE hi₁₂) (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂)
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
/-- A function is $C^{0+(α)}$ at a point if and only if
it is $C^0$ at the point (i.e., it is continuous on a neighborhood of the point)
and $f(x) - f(a) = O(‖x - a‖ ^ α)$.  -/
ContDiffPointwiseHolderAt.zero_order_iff : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {α : ↑unitInterval} {f : E → F} {a : E},
  ContDiffPointwiseHolderAt 0 α f a ↔ ContDiffAt ℝ 0 f a ∧ (fun x => f x - f a) =O[nhds a] fun x => ‖x - a‖ ^ ↑α
-- Mathlib.CategoryTheory.Adjunction.Opposites
CategoryTheory.Functor.IsLeftAdjoint.rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor Cᵒᵖ D} [F.IsLeftAdjoint], F.rightOp.IsRightAdjoint
-- Mathlib.Topology.Separation.Basic
/-- In an R₀ space, `Specializes` is equivalent to `Inseparable`.  -/
specializes_iff_inseparable : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R0Space X] {x y : X}, x ⤳ y ↔ Inseparable x y
-- Mathlib.Order.Nucleus
Nucleus.le_apply : ∀ {X : Type u_1} [inst : SemilatticeInf X] {n : Nucleus X} {x : X}, x ≤ n x
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.ofFixingSubgroup_insert_map.eq_1 : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] (a : α)
  (s : Set ↥(SubMulAction.ofStabilizer M a)),
  SubMulAction.ofFixingSubgroup_insert_map a s =
    { toFun := fun x => (fun hx hx' => ⟨⟨↑x, hx⟩, hx'⟩) ⋯ ⋯, map_smul' := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- Two vertices are adjacent iff there is an edge between them. The
condition `v ≠ w` ensures they are different endpoints of the edge,
which is necessary since when `v = w` the existential
`∃ (e ∈ G.edgeSet), v ∈ e ∧ w ∈ e` is satisfied by every edge
incident to `v`.  -/
SimpleGraph.adj_iff_exists_edge : ∀ {V : Type u} {G : SimpleGraph V} {v w : V}, G.Adj v w ↔ v ≠ w ∧ ∃ e ∈ G.edgeSet, v ∈ e ∧ w ∈ e
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey!_empty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α],
  ∅.maxKey! = default
-- Mathlib.Data.Finset.Max
Finset.min'_le_max' : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (hs : s.Nonempty), s.min' hs ≤ s.max' hs
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.TauPackage.color.eq_def : ∀ {α : Type u_1} [inst : MetricSpace α] {β : Type u} [inst_1 : Nonempty β] (p : Besicovitch.TauPackage β α)
  (x : Ordinal.{u}),
  p.color x =
    have i := x;
    have A :=
      ⋃ j,
        ⋃ (_ :
          (Metric.closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩
              Metric.closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
          {p.color ↑j};
    sInf (Set.univ \ A)
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.equivProdDFinsupp_symm_apply : ∀ {ι : Type u} {α : Option ι → Type v} [inst : (i : Option ι) → Zero (α i)] (f : α none × Π₀ (i : ι), α (some i)),
  DFinsupp.equivProdDFinsupp.symm f = DFinsupp.extendWith f.1 f.2
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- The Mellin transform of `P.f` is globally convergent. Private since it is superseded by
`IsStrongFEPair.hasMellin` below, which also identifies its Mellin transform as `P.Λ`.  -/
_private.Mathlib.NumberTheory.LSeries.AbstractFuncEq.0.IsStrongFEPair.mellinConvergent : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {P : WeakFEPair E},
  IsStrongFEPair P → ∀ (s : ℂ), MellinConvergent P.f s
-- Mathlib.Order.Max
IsBot.mono : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, IsBot a → b ≤ a → IsBot b
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_s₁_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  [inst_1 : E.HasPullbacks] {i j : E.toPreOneHypercover.I₀} (k : E.toPreOneHypercover.I₁ i j),
  (E.toSaturateOfHasPullbacks.s₁ k).snd = CategoryTheory.Limits.pullback.snd (E.f i) (E.f j)
-- Mathlib.Algebra.Group.Submonoid.Defs
SubmonoidClass.toMulMemClass : ∀ {S : Type u_3} {M : outParam (Type u_4)} {inst : MulOneClass M} {inst_1 : SetLike S M} [self : SubmonoidClass S M],
  MulMemClass S M
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.differentiable_completedCosZeta₀ : ∀ (a : UnitAddCircle), Differentiable ℂ (HurwitzZeta.completedCosZeta₀ a)
-- Mathlib.Analysis.Normed.Algebra.MatrixExponential
Matrix.BlockTriangular.exp : ∀ {m : Type u_1} {α : Type u_4} {𝔸 : Type u_5} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : Ring 𝔸]
  [inst_3 : TopologicalSpace 𝔸] [inst_4 : IsTopologicalRing 𝔸] [T2Space 𝔸] [inst_6 : LinearOrder α] [Algebra ℚ 𝔸]
  {M : Matrix m m 𝔸} {b : m → α}, M.BlockTriangular b → (NormedSpace.exp M).BlockTriangular b
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.nullHomotopy_hom : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (hom : (i j : ι) → C.X i ⟶ D.X j)
  (zero : ∀ (i j : ι), ¬c.Rel j i → hom i j = 0) (i j : ι), (Homotopy.nullHomotopy hom zero).hom i j = hom i j
-- Lean.Elab.DeclModifiers
/-- The docstring, if present.
 -/
Lean.Elab.Modifiers.docString? : Lean.Elab.Modifiers → Option (Lean.TSyntax `Lean.Parser.Command.docComment)
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.norm_natCast : ∀ {R : Type u_2} {a b : R} [inst : CommRing R] (n : ℕ), QuadraticAlgebra.norm ↑n = ↑n ^ 2
-- Mathlib.Combinatorics.Graph.Maps
Graph.IsLink.map : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_4} {G : Graph α β} {u v : α} {e : β} (f : α → α'),
  G.IsLink e u v → (Graph.map f G).IsLink e (f u) (f v)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift.0.Std.Iterators.Types.ULiftIterator.Monadic.modifyStep.match_1.eq_3 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.Logic.Equiv.Defs
Equiv.invFun_as_coe : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.invFun = ⇑e.symm
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.continuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsLocallyConstant f → Continuous f
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isSome_minKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β k}, (t.insertIfNew k v).minKey?.isSome = true
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.instAdditiveHomotopyCategoryIntUpQh : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C], DerivedCategory.Qh.Additive
-- Mathlib.Analysis.Convex.Cone.InnerDual
ProperCone.innerDual_toSubmodule : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : CompleteSpace E] (s : Set E),
  ↑(ProperCone.innerDual s) = PointedCone.dual (innerₗ E) s
-- Mathlib.Combinatorics.Enumerative.Bell
Nat.bell.eq_2 : ∀ (n : ℕ), n.succ.bell = ∑ i ≤ n, n.choose i * (n - i).bell
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.IsNegInvariant.mk : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Neg G] {μ : MeasureTheory.Measure G}, μ.neg = μ → μ.IsNegInvariant
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLinearMapRight'_mul_apply : ∀ {R : Type u_1} [inst : Semiring R] {l : Type u_2} {m : Type u_3} {n : Type u_4} [inst_1 : Fintype m]
  [inst_2 : DecidableEq m] [inst_3 : Fintype l] [inst_4 : DecidableEq l] (M : Matrix l m R) (N : Matrix m n R)
  (x : l → R), (Matrix.toLinearMapRight' (M * N)) x = (Matrix.toLinearMapRight' N) ((Matrix.toLinearMapRight' M) x)
-- Mathlib.Order.Comparable
compRel_of_total : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Total r] (a b : α), CompRel r a b
-- Init.MetaTypes
/-- If `instances` is `true`, `simp` will visit instance arguments.
If option `backward.dsimp.instances` is `true`, it overrides this field.
 -/
Lean.Meta.Simp.Config.instances : Lean.Meta.Simp.Config → Bool
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- Two 2-morphisms out of a left Kan extension are equal if their compositions with
each triangle 2-morphism are equal.  -/
CategoryTheory.Bicategory.LeftExtension.IsKan.hom_ext : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  {t : CategoryTheory.Bicategory.LeftExtension f g} (H : t.IsKan) {k : b ⟶ c} {τ τ' : t.extension ⟶ k},
  CategoryTheory.CategoryStruct.comp t.unit (CategoryTheory.Bicategory.whiskerLeft f τ) =
      CategoryTheory.CategoryStruct.comp t.unit (CategoryTheory.Bicategory.whiskerLeft f τ') →
    τ = τ'
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Zero.mk.injEq : ∀ {α : Type} (state state_1 : Std.Mutex (Std.CloseableChannel.Zero.State✝ α)),
  ({ state := state } = { state := state_1 }) = (state = state_1)
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.hom_ext : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (f g : S₁ ⟶ S₂), f.τ₁ = g.τ₁ → f.τ₂ = g.τ₂ → f.τ₃ = g.τ₃ → f = g
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.Subcomplex.coe_copy`. -/
Topology.CWComplex.Subcomplex.coe_copy : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  (E : Topology.RelCWComplex.Subcomplex C) (F : Set X) (hF : F = ↑E)
  (J : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) (hJ : J = E.I), ↑(E.copy F hF J hJ) = F
-- Mathlib.InformationTheory.KullbackLeibler.KLFun
/-- `klFun` is strictly convex on $[0,∞)$.  -/
InformationTheory.strictConvexOn_klFun : StrictConvexOn ℝ (Set.Ici 0) InformationTheory.klFun
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.singleton_vsub : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] [inst_1 : DecidableEq α] {t : Finset β} (a : β),
  {a} -ᵥ t = Finset.image (fun x => a -ᵥ x) t
-- Mathlib.CategoryTheory.Preadditive.Comma
CategoryTheory.CommaMorphism.zero_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Preadditive A] {B : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} B] [inst_3 : CategoryTheory.Preadditive B] {T : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} T] [inst_5 : CategoryTheory.Preadditive T] (L : CategoryTheory.Functor A T)
  [inst_6 : L.Additive] (R : CategoryTheory.Functor B T) [inst_7 : R.Additive] {u v : CategoryTheory.Comma L R},
  CategoryTheory.CommaMorphism.right 0 = 0
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- **Alias** of `QuadraticForm.isSymm_toMatrix'`. -/
QuadraticForm.QuadraticMap.isSymm_toMatrix' : ∀ {R : Type u_3} {n : Type w} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] [inst_3 : Invertible 2]
  (Q : QuadraticForm R (n → R)), Q.toMatrix'.IsSymm
-- Mathlib.AlgebraicGeometry.AffineSpace
CategoryTheory.MorphismProperty.isomorphisms.eq_1 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (x x_1 : C) (f : x ⟶ x_1),
  CategoryTheory.MorphismProperty.isomorphisms C f = CategoryTheory.IsIso f
-- Init.Data.Float.Float32
instSubFloat32 : Sub Float32
-- Mathlib.Data.Set.MulAntidiagonal
Set.MulAntidiagonal.finite_of_isPWO : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] [IsCancelMul α] [MulLeftMono α] [MulRightStrictMono α]
  {s t : Set α}, s.IsPWO → t.IsPWO → ∀ (a : α), (s.mulAntidiagonal t a).Finite
-- Mathlib.Algebra.Group.Defs
zero_nsmul : ∀ {M : Type u_2} [inst : AddMonoid M] (a : M), 0 • a = 0
-- Mathlib.FieldTheory.RatFunc.Luroth
/-- A polynomial `b` that satisfies `b * φ = Φ'`.  -/
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.b : {K : Type u_1} → [inst : Field K] → IntermediateField K (RatFunc K) → Polynomial K
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
Submodule.localized'_span : ∀ {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Algebra R S] [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] (p : Submonoid R)
  [inst_9 : IsLocalization p S] (f : M →ₗ[R] N) [inst_10 : IsLocalizedModule p f] (s : Set M),
  Submodule.localized' S p f (Submodule.span R s) = Submodule.span S (⇑f '' s)
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.measurableSet_succ_countablePartition : ∀ {α : Type u_1} [m : MeasurableSpace α] [h : MeasurableSpace.CountablyGenerated α] (n : ℕ) {s : Set α},
  s ∈ MeasurableSpace.countablePartition α n → MeasurableSet s
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {a : α}, t.isEmpty = true → t.getKey! a = default
-- Mathlib.Tactic.MoveAdd
/-- `permuteExpr op tgt instructions` takes the same input as `rankSums` and returns the
expression obtained from `tgt` by replacing all `old_sum`s by the corresponding `new_sum`.
If there were no required changes, then `permuteExpr` reports this in its second factor.  -/
Mathlib.MoveAdd.permuteExpr : Lean.Name → Lean.Expr → List (Lean.Expr × Bool) → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.monFunctorCategoryEquivalence_inverse : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D],
  (CategoryTheory.Monoidal.monFunctorCategoryEquivalence C D).inverse =
    CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.ratio_of_trivial : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F),
  (∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤) → Dilation.ratio f = 1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {a : α}, ∅.getKey? a = none
-- Lean.Util.PtrSet
Lean.PtrSet.insert : {α : Type} → Lean.PtrSet α → α → Lean.PtrSet α
-- Mathlib.Algebra.Group.Commute.Units
Units.ofPowEqOne.congr_simp : ∀ {M : Type u_1} [inst : Monoid M] (a a_1 : M) (e_a : a = a_1) (n n_1 : ℕ) (e_n : n = n_1) (ha : a ^ n = 1)
  (hn : n ≠ 0), Units.ofPowEqOne a n ha hn = Units.ofPowEqOne a_1 n_1 ⋯ ⋯
-- Mathlib.RingTheory.WittVector.TeichmullerSeries
/-- Given a ring `S` such that `p` is nilpotent in `S`
and two ring maps `f g : 𝕎 R →+* S`, if they coincide on the teichmuller representatives,
then they are equal.
 -/
WittVector.eq_of_apply_teichmuller_eq : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {R : Type u_1} [inst : CommRing R] [CharP R p] [PerfectRing R p] {S : Type u_2}
  [inst_3 : CommRing S] (f g : WittVector p R →+* S),
  IsNilpotent ↑p → (∀ (x : R), f ((WittVector.teichmuller p) x) = g ((WittVector.teichmuller p) x)) → f = g
-- Mathlib.CategoryTheory.Limits.Types.Colimits
CategoryTheory.Limits.colimit.ι_map_apply : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J C]
  {G : CategoryTheory.Functor J C} (α : F ⟶ G) (j : J) {F_1 : C → C → Type uF} {carrier : C → Type w}
  {instFunLike : (X Y : C) → FunLike (F_1 X Y) (carrier X) (carrier Y)} [inst_3 : CategoryTheory.ConcreteCategory C F_1]
  (x : carrier (F.obj j)),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimMap α))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) x) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι G j))
      ((CategoryTheory.ConcreteCategory.hom (α.app j)) x)
-- Mathlib.Topology.EMetricSpace.Diam
Metric.ediam_eball_le : ∀ {X : Type u_2} {x : X} [inst : PseudoEMetricSpace X] {r : ENNReal}, Metric.ediam (Metric.eball x r) ≤ 2 * r
-- Mathlib.Probability.HasLaw
ProbabilityTheory.HasLaw.measureReal_eq : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {μ : MeasureTheory.Measure 𝓧} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.HasLaw X μ P → ∀ {p : 𝓧 → Prop}, MeasurableSet {x | p x} → P.real {ω | p (X ω)} = μ.real {x | p x}
-- Init.Data.Nat.Internal.SOM
_private.Init.Data.Nat.Internal.SOM.0.Nat.Internal.SOM.Poly.add.go : ℕ → Nat.Internal.SOM.Poly → Nat.Internal.SOM.Poly → Nat.Internal.SOM.Poly
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
AddSubmonoid.apply_ne_zero_of_mem_or_neg_mem_closure : ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : AddCommGroup G] [inst_1 : LinearOrder S]
  [inst_2 : InvolutiveNeg ι] [inst_3 : AddCommGroup S] [IsOrderedAddMonoid S] (v : ι → G) (f : G →+ S) (s : Set ι),
  (∀ i ∈ s, 0 < f (v i)) →
    ∀ (i : ι),
      v i ≠ 0 → v (-i) = -v i → v i ∈ AddSubmonoid.closure (v '' s) ∨ -v i ∈ AddSubmonoid.closure (v '' s) → f (v i) ≠ 0
-- Mathlib.LinearAlgebra.Matrix.Basis
Module.Basis.sum_toMatrix_smul_self : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (e : Module.Basis ι R M) (v : ι' → M) (j : ι') [inst_3 : Fintype ι],
  ∑ i, e.toMatrix v i j • e i = v j
-- Init.Data.Vector.Monadic
Vector.findM?_pure : ∀ {α : Type} {n : ℕ} {m : Type → Type} [inst : Monad m] [LawfulMonad m] {p : α → Bool} {xs : Vector α n},
  Vector.findM? (fun x => pure (p x)) xs = pure (Vector.find? p xs)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trNum.eq_2 : ∀ (n : PosNum), Turing.PartrecToTM2.trNum (Num.pos n) = Turing.PartrecToTM2.trPosNum n
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.node4L_lemma₂ : ∀ {b c d : ℕ}, b + c + 1 ≤ 3 * d → c ≤ 3 * d
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Array
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.Array.0.Std.Types.ListIterator.stepAsHetT_iterM.match_1.eq_1 : ∀ {β : Type u_1} (motive : List β → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (x : β) → (xs : List β) → motive (x :: xs)),
  (match [] with
    | [] => h_1 ()
    | x :: xs => h_2 x xs) =
    h_1 ()
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinite_neg : ∀ {x : ℝ*}, (-x).Infinite ↔ x.Infinite
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.curry₃_obj_obj_obj_map : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃]
  [inst_3 : CategoryTheory.Category.{v_9, u_9} E] (F : CategoryTheory.Functor (C₁ × C₂ × C₃) E) (X₁ : C₁) (X₂ : C₂)
  {X₃ Y₃ : C₃} (f : X₃ ⟶ Y₃),
  (((CategoryTheory.Functor.curry₃.obj F).obj X₁).obj X₂).map f =
    F.map (CategoryTheory.CategoryStruct.id X₁, CategoryTheory.CategoryStruct.id X₂, f)
-- Mathlib.Order.Bounds.Lattice
isGLB_iUnion_iff_of_isLUB : ∀ {α : Type u_1} [inst : Preorder α] {ι : Sort u_2} {s : ι → Set α} {u : ι → α},
  (∀ (i : ι), IsGLB (s i) (u i)) → ∀ (c : α), IsGLB (Set.range u) c ↔ IsGLB (⋃ i, s i) c
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
/-- The category structure on `∫ᶜ F`.  -/
CategoryTheory.Pseudofunctor.CoGrothendieck.category : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} →
      CategoryTheory.Category.{max v₁ v₂, max u₂ u₁} F.CoGrothendieck
-- Init.Data.SInt.Lemmas
Int16.toBitVec_neg : ∀ (x : Int16), (-x).toBitVec = -x.toBitVec
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF.measure_ge_le_exp_add : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {κ : ProbabilityTheory.Kernel Ω' Ω} {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.Kernel.HasSubgaussianMGF X c κ ν →
    ∀ (ε : ℝ), ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), 0 ≤ t → (κ ω').real {ω | ε ≤ X ω} ≤ Real.exp (-t * ε + ↑c * t ^ 2 / 2)
-- Mathlib.Algebra.Algebra.Equiv
/-- **Alias** of `AlgEquiv.ofAlgHom_toAlgHom`. -/
AlgEquiv.ofAlgHom_coe_algHom : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (f : A₁ ≃ₐ[R] A₂) (g : A₂ →ₐ[R] A₁)
  (h₁ : (↑f).comp g = AlgHom.id R A₂) (h₂ : g.comp ↑f = AlgHom.id R A₁), AlgEquiv.ofAlgHom (↑f) g h₁ h₂ = f
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.apply_def : ∀ {X : TopCat} {U V : TopologicalSpace.Opens ↑X} (f : U ⟶ V) (x : ↥U), f x = ⟨↑x, ⋯⟩