mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_alter_eq_isEmpty_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {f : Option β → Option β}, (t.alter k f).isEmpty = ((t.erase k).isEmpty && (f t[k]?).isNone)
-- Mathlib.CategoryTheory.Distributive.Monoidal
CategoryTheory.coprod_inr_leftDistrib_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_3 : CategoryTheory.IsMonoidalLeftDistrib C] {X Y Z : C},
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.leftDistrib X Y Z).hom =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.coprod.inr
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.InvariantForm.mk.injEq : ∀ {ι : 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}
  (form : LinearMap.BilinForm R M) (symm : LinearMap.IsSymm form)
  (ne_zero : ∀ (i : ι), (form (P.root i)) (P.root i) ≠ 0)
  (isOrthogonal_reflection : ∀ (i : ι), LinearMap.IsOrthogonal form ⇑(P.reflection i))
  (form_1 : LinearMap.BilinForm R M) (symm_1 : LinearMap.IsSymm form_1)
  (ne_zero_1 : ∀ (i : ι), (form_1 (P.root i)) (P.root i) ≠ 0)
  (isOrthogonal_reflection_1 : ∀ (i : ι), LinearMap.IsOrthogonal form_1 ⇑(P.reflection i)),
  ({ form := form, symm := symm, ne_zero := ne_zero, isOrthogonal_reflection := isOrthogonal_reflection } =
      { form := form_1, symm := symm_1, ne_zero := ne_zero_1, isOrthogonal_reflection := isOrthogonal_reflection_1 }) =
    (form = form_1)
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveView.declId : Lean.Elab.Command.InductiveView → Lean.Syntax
-- Mathlib.Topology.Bornology.Hom
/-- The function underlying a locally bounded map  -/
LocallyBoundedMap.toFun : {α : Type u_6} → {β : Type u_7} → [inst : Bornology α] → [inst_1 : Bornology β] → LocallyBoundedMap α β → α → β
-- Mathlib.Data.Nat.Factorization.Basic
Nat.ordProj_mul : ∀ {a b : ℕ} (p : ℕ), a ≠ 0 → b ≠ 0 → p ^ (a * b).factorization p = p ^ a.factorization p * p ^ b.factorization p
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.WF.empty : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α], ∅.WF
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
_private.Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic.0.CategoryTheory.Limits.compNatIso.match_1.splitter : (motive : CategoryTheory.Limits.WalkingParallelPair → Sort u_1) →
  (j : CategoryTheory.Limits.WalkingParallelPair) →
    (Unit → motive CategoryTheory.Limits.WalkingParallelPair.zero) →
      (Unit → motive CategoryTheory.Limits.WalkingParallelPair.one) → motive j
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.isInducedSubgraph_bot_iff : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β}, G.IsInducedSubgraph ⊥ ↔ G = ⊥
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- Given a costructured arrow `s : yoneda.obj X ⟶ A` and an element `x : F.obj s`, construct
an element of `YonedaCollection F X`.  -/
CategoryTheory.OverPresheafAux.YonedaCollection.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} →
        {X : C} →
          (s : CategoryTheory.yoneda.obj X ⟶ A) →
            F.obj (Opposite.op (CategoryTheory.CostructuredArrow.mk s)) →
              CategoryTheory.OverPresheafAux.YonedaCollection F X
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.app_appIso_inv : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f U)
      (AlgebraicGeometry.Scheme.Hom.appIso f ((TopologicalSpace.Opens.map f.base).obj U)).inv =
    Y.presheaf.map (CategoryTheory.homOfLE ⋯).op
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.fderivLM_apply_of_gt : ∀ (𝕜 : 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] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n k : ℕ∞} {K : TopologicalSpace.Compacts E} (f : ContDiffMapSupportedIn E F n K),
  n < k + 1 → (ContDiffMapSupportedIn.fderivLM 𝕜 n k) f = 0
-- Mathlib.RingTheory.Polynomial.Wronskian
Polynomial.wronskian_add_right : ∀ {R : Type u_1} [inst : CommRing R] (a b c : Polynomial R), a.wronskian (b + c) = a.wronskian b + a.wronskian c
-- Init.Data.Float.Float32
/-- Converts a `Float32` into a `Float32.Model`.  -/
Float32.toModel : Float32 → Float32.Model
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.SymmStruct.iso_hom_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type w}
  {I : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C} (self : I.SymmStruct)
  (i j : ι), CategoryTheory.CategoryStruct.comp (self.iso i j).hom (I.snd (j, i)) = I.fst (i, j)
-- Lean.Elab.Command
Lean.Elab.Command.Linter.mk.inj : ∀ {run : Lean.Syntax → Lean.Elab.Command.CommandElabM Unit}
  {name : autoParam Lean.Name Lean.Elab.Command.Linter.name._autoParam}
  {run_1 : Lean.Syntax → Lean.Elab.Command.CommandElabM Unit}
  {name_1 : autoParam Lean.Name Lean.Elab.Command.Linter.name._autoParam},
  { run := run, name := name } = { run := run_1, name := name_1 } → run = run_1 ∧ name = name_1
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.isCardinalPresentable_of_le : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalPresentable X κ] {κ' : Cardinal.{w}} [inst_3 : Fact κ'.IsRegular],
  κ ≤ κ' → CategoryTheory.IsCardinalPresentable X κ'
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.coe_uniqueProd : ∀ (R : Type u_8) (M : Type u_9) (N : Type u_10) [inst : Semiring R] [inst_1 : TopologicalSpace M]
  [inst_2 : AddCommMonoid M] [inst_3 : TopologicalSpace N] [inst_4 : AddCommMonoid N] [inst_5 : Unique N]
  [inst_6 : Module R M] [inst_7 : Module R N],
  (↑(ContinuousLinearEquiv.uniqueProd R M N)).toEquiv = Equiv.uniqueProd M N
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeAction.mk.inj : ∀ {toWorkDoneProgressParams : Lean.Lsp.WorkDoneProgressParams} {toPartialResultParams : Lean.Lsp.PartialResultParams}
  {title : String} {kind? : Option Lean.Lsp.CodeActionKind} {diagnostics? : Option (Array Lean.Lsp.Diagnostic)}
  {isPreferred? : Option Bool} {disabled? : Option Lean.Lsp.CodeActionDisabled} {edit? : Option Lean.Lsp.WorkspaceEdit}
  {command? : Option Lean.Lsp.Command} {data? : Option Lean.Json}
  {toWorkDoneProgressParams_1 : Lean.Lsp.WorkDoneProgressParams}
  {toPartialResultParams_1 : Lean.Lsp.PartialResultParams} {title_1 : String} {kind?_1 : Option Lean.Lsp.CodeActionKind}
  {diagnostics?_1 : Option (Array Lean.Lsp.Diagnostic)} {isPreferred?_1 : Option Bool}
  {disabled?_1 : Option Lean.Lsp.CodeActionDisabled} {edit?_1 : Option Lean.Lsp.WorkspaceEdit}
  {command?_1 : Option Lean.Lsp.Command} {data?_1 : Option Lean.Json},
  { toWorkDoneProgressParams := toWorkDoneProgressParams, toPartialResultParams := toPartialResultParams,
        title := title, kind? := kind?, diagnostics? := diagnostics?, isPreferred? := isPreferred?,
        disabled? := disabled?, edit? := edit?, command? := command?, data? := data? } =
      { toWorkDoneProgressParams := toWorkDoneProgressParams_1, toPartialResultParams := toPartialResultParams_1,
        title := title_1, kind? := kind?_1, diagnostics? := diagnostics?_1, isPreferred? := isPreferred?_1,
        disabled? := disabled?_1, edit? := edit?_1, command? := command?_1, data? := data?_1 } →
    toWorkDoneProgressParams = toWorkDoneProgressParams_1 ∧
      toPartialResultParams = toPartialResultParams_1 ∧
        title = title_1 ∧
          kind? = kind?_1 ∧
            diagnostics? = diagnostics?_1 ∧
              isPreferred? = isPreferred?_1 ∧
                disabled? = disabled?_1 ∧ edit? = edit?_1 ∧ command? = command?_1 ∧ data? = data?_1
-- Mathlib.Topology.MetricSpace.Infsep
Set.relatively_discrete_of_finite : ∀ {α : Type u_1} [inst : EMetricSpace α] {s : Set α} [Finite ↑s], ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
/-- A Fredholm operator has (topologically) complemented range.  -/
ContinuousLinearMap.IsFredholm.closedComplemented_range : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E]
  [inst_6 : TopologicalSpace F] [CompleteSpace 𝕜] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] {u : E →L[𝕜] F},
  u.IsFredholm → (↑u).range.ClosedComplemented
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.IsGenerating.eq_1 : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (C : ConvexCone R M), C.IsGenerating = (Submodule.span R ↑C = ⊤)
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
ChevalleyThm.MvPolynomialC.degBound_pos : ∀ (k : ℕ) (D : ℕ → ℕ) (n : ℕ), 0 < ChevalleyThm.MvPolynomialC.degBound k D n
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIcc_subset_Icc : ∀ {α : Type u_1} [inst : Lattice α] {a₁ a₂ b₁ b₂ : α},
  a₁ ∈ Set.Icc a₂ b₂ → b₁ ∈ Set.Icc a₂ b₂ → Set.uIcc a₁ b₁ ⊆ Set.Icc a₂ b₂
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.instReprBVBit : Repr Std.Tactic.BVDecide.BVBit
-- Std.Time.Time.Unit.Second
Std.Time.Second.instToStringOffset : ToString Std.Time.Second.Offset
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.instLawfulToBackwardSearcherModelForallCharPropDefaultBackwardSearcherForallBoolDecide : ∀ {p : Char → Prop} [inst : DecidablePred p], String.Slice.Pattern.Model.LawfulToBackwardSearcherModel p
-- Mathlib.Order.SuccPred.CompleteLinearOrder
IsLUB.exists_of_nonempty_of_not_isSuccLimit : ∀ {ι : Sort u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [Nonempty ι] {f : ι → α} {x : α},
  IsLUB (Set.range f) x → ¬Order.IsSuccLimit x → ∃ i, f i = x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t t_1 : Std.DTreeMap α β cmp) (e_t : t = t_1) (a a_1 : α)
  (e_a : a = a_1) (h : a ∈ t), t.getKey a h = t_1.getKey a_1 ⋯
-- Mathlib.Topology.ContinuousOn
isOpenMap_prod_of_discrete_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [DiscreteTopology α] {f : α × β → γ},
  IsOpenMap f ↔ ∀ (a : α), IsOpenMap fun x => f (a, x)
-- Mathlib.Data.List.Cycle
List.prev_cons_cons_eq' : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (x y z : α) (h : x ∈ y :: z :: l),
  x = y → (y :: z :: l).prev x h = (z :: l).getLast ⋯
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.WhiskerLeft.whisker.sizeOf_spec : ∀ (e : Mathlib.Tactic.BicategoryLike.Mor₂) (f : Mathlib.Tactic.BicategoryLike.Atom₁)
  (η : Mathlib.Tactic.BicategoryLike.WhiskerLeft),
  sizeOf (Mathlib.Tactic.BicategoryLike.WhiskerLeft.whisker e f η) = 1 + sizeOf e + sizeOf f + sizeOf η
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.Iterator.instLawfulDeterministicIterator : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α],
  Std.LawfulDeterministicIterator (Std.Rxo.Iterator α) Id
-- Mathlib.Algebra.Quaternion
Quaternion.ext_iff : ∀ {R : Type u_3} [inst : CommRing R] {a b : Quaternion R},
  a = b ↔ a.re = b.re ∧ a.imI = b.imI ∧ a.imJ = b.imJ ∧ a.imK = b.imK
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- If `G.IsBipartiteWith s t`, then the sum of the degrees of vertices in `s` is equal to the sum
of the degrees of vertices in `t`.

See `Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow`.  -/
SimpleGraph.isBipartiteWith_sum_degrees_eq : ∀ {V : Type u_1} {G : SimpleGraph V} {s t : Finset V} [inst : G.LocallyFinite],
  G.IsBipartiteWith ↑s ↑t → ∑ v ∈ s, G.degree v = ∑ w ∈ t, G.degree w
-- Init.Data.Format.Basic
/-- `align` tells the formatter to pad with spaces to the current indentation level, or else add a
newline if we are already at or past the indent.

If `force` is true, then it will pad to the indent even if it is in a flattened group.

Example:
```lean example
open Std Format in
#eval IO.println (nest 2 <| "." ++ align ++ "a" ++ line ++ "b")
```
```lean output
. a
  b
```
 -/
Std.Format.align : Bool → Std.Format
-- Mathlib.Algebra.Lie.Prod
LieHom.prodMap_comp : ∀ {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} {L₃ : Type u_5} {L₄ : Type u_6} {L₅ : Type u_7} {L₆ : Type u_8}
  [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁] [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂]
  [inst_5 : LieRing L₃] [inst_6 : LieAlgebra R L₃] [inst_7 : LieRing L₄] [inst_8 : LieAlgebra R L₄]
  [inst_9 : LieRing L₅] [inst_10 : LieAlgebra R L₅] [inst_11 : LieRing L₆] [inst_12 : LieAlgebra R L₆]
  (f₁₂ : L₁ →ₗ⁅R⁆ L₂) (f₂₃ : L₂ →ₗ⁅R⁆ L₃) (g₁₂ : L₄ →ₗ⁅R⁆ L₅) (g₂₃ : L₅ →ₗ⁅R⁆ L₆),
  (f₂₃.prodMap g₂₃).comp (f₁₂.prodMap g₁₂) = (f₂₃.comp f₁₂).prodMap (g₂₃.comp g₁₂)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_union_iff : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∈ m₁ ∪ m₂ ↔ k ∈ m₁ ∨ k ∈ m₂
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Given a localization map `f : M →+ N`, a section function sending `z : N`
to some `(x, y) : M × S` such that `f x - f y = z`.  -/
AddSubmonoid.LocalizationMap.sec : {M : Type u_1} →
  [inst : AddCommMonoid M] →
    {S : AddSubmonoid M} → {N : Type u_2} → [inst_1 : AddCommMonoid N] → S.LocalizationMap N → N → M × ↥S
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {k : α} {v : β}, (t.insert k v)[k]! = v
-- Mathlib.Analysis.Distribution.Support
Distribution.TemperedDistribution.IsVanishingOn.iteratedLineDerivOp : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ E]
  [inst_3 : NormedSpace ℂ F] {f : TemperedDistribution E F} {s : Set E} {n : ℕ},
  Distribution.IsVanishingOn (⇑f) s →
    ∀ (m : Fin n → E), Distribution.IsVanishingOn (⇑(LineDeriv.iteratedLineDerivOp m f)) s
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.sub : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {l : Filter α} {f₁ f₂ : α → E'}, f₁ =O[l] g → f₂ =O[l] g → (fun x => f₁ x - f₂ x) =O[l] g
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.map.comp : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (g : β → γ) (x : FreeGroup α),
  (FreeGroup.map g) ((FreeGroup.map f) x) = (FreeGroup.map (g ∘ f)) x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_le_size_insertMany!_list : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF → ∀ {l : List (α × β)}, t.size ≤ (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l)).size
-- Init.Data.Option.Array
Option.size_toArray_le : ∀ {α : Type u_1} {o : Option α}, o.toArray.size ≤ 1
-- Mathlib.Algebra.Category.ModuleCat.Abelian
/-- The category of R-modules is abelian.  -/
ModuleCat.abelian : {R : Type u} → [inst : Ring R] → CategoryTheory.Abelian (ModuleCat R)
-- Lean.Meta.Tactic.Grind.Split
_private.Lean.Meta.Tactic.Grind.Split.0.Lean.Meta.Grind.checkForallStatus : (imp : Lean.Expr) → imp.isForall = true → Lean.Meta.Grind.GoalM Lean.Meta.Grind.SplitStatus
-- Mathlib.Analysis.Calculus.Deriv.Add
deriv_add : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {x : 𝕜},
  DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 g x → deriv (f + g) x = deriv f x + deriv g x
-- Mathlib.Data.Countable.Defs
instUncountableULift : ∀ {β : Type v} [Uncountable β], Uncountable (ULift.{u, v} β)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insertIfNew k v).minKey ⋯ = t.minKey?.elim k fun k' => if cmp k k' = Ordering.lt then k else k'
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.Const.get!ₘ : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → [Inhabited β] → (Std.DHashMap.Internal.Raw₀ α fun x => β) → α → β
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
LinearPMap.adjoint.congr_simp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  (T T_1 : E →ₗ.[𝕜] F), T = T_1 → ∀ [inst_5 : CompleteSpace E], T.adjoint = T_1.adjoint
-- Init.Data.Vector.Lex
Vector.lex_toArray : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] {lt : α → α → Bool} {xs ys : Vector α n},
  xs.toArray.lex ys.toArray lt = xs.lex ys lt
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.toNat_toInt_add_one_sub_toInt : ∀ {n : ℕ} {lo hi : BitVec n},
  n > 0 → (hi.toInt + 1 - lo.toInt).toNat = (BitVec.Signed.rotate✝ hi).toNat + 1 - (BitVec.Signed.rotate✝ lo).toNat
-- Mathlib.Order.Minimal
minimal_true : ∀ {α : Type u_2} {x : α} [inst : LE α], Minimal (fun x => True) x ↔ IsMin x
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
/-- Recursor on walks by inducting on `SimpleGraph.Walk.concat`.

This is inducting from the opposite end of the walk compared
to `SimpleGraph.Walk.rec`, which inducts on `SimpleGraph.Walk.cons`.  -/
SimpleGraph.Walk.concatRec : {V : Type u} →
  {G : SimpleGraph V} →
    {motive : (u v : V) → G.Walk u v → Sort u_1} →
      ({u : V} → motive u u SimpleGraph.Walk.nil) →
        ({u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)) →
          {u v : V} → (p : G.Walk u v) → motive u v p
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.singleton_eq_insert : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {a : α}, {a} = ∅.insert a
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.subst_substInvOfIsUnit_right : ∀ {R : Type u_2} [inst : CommRing R] (P : PowerSeries R),
  PowerSeries.constantCoeff P = 0 →
    ∀ (hP' : IsUnit ((PowerSeries.coeff 1) P)), PowerSeries.subst (P.substInvOfIsUnit hP') P = PowerSeries.X
-- Mathlib.Data.Fin.Parity
Fin.even_iff_imp : ∀ {n : ℕ} {k : Fin n}, Even k ↔ Even n → Even ↑k
-- Mathlib.Condensed.Light.Small
CategoryTheory.SmallModel.congr_simp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.EssentiallySmall.{w, v, u} C],
  CategoryTheory.SmallModel.{w, v, u} C = CategoryTheory.SmallModel.{w, v, u} C
-- Init.Data.List.Lemmas
List.reverse_singleton : ∀ {α : Type u_1} {a : α}, [a].reverse = [a]
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.isBounded_image_ofSnowflaking_iff : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : Bornology X] {s : Set (Metric.Snowflaking X α hα₀ hα₁)},
  Bornology.IsBounded (⇑Metric.Snowflaking.ofSnowflaking '' s) ↔ Bornology.IsBounded s
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.singleton_sdiv_singleton : ∀ {α : Type u_2} {β : Type u_3} [inst : SDiv α β] {b c : β}, {b} /ₛ {c} = {b /ₛ c}
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.prod_le_prod_of_rel_le : ∀ {α : Type u_2} [inst : CommMonoid α] [inst_1 : Preorder α] {s t : Multiset α} [MulLeftMono α],
  Multiset.Rel (fun x1 x2 => x1 ≤ x2) s t → s.prod ≤ t.prod
-- Mathlib.CategoryTheory.MorphismProperty.Retract
CategoryTheory.MorphismProperty.IsStableUnderRetracts.isomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.MorphismProperty.isomorphisms C).IsStableUnderRetracts
-- Mathlib.Combinatorics.SetFamily.KruskalKatona
/-- This measures roughly how compressed the family is.

Note that this does depend on the order of the ground set, unlike the Kruskal-Katona theorem itself
(although `kruskal_katona` currently is stated in an order-dependent manner).  -/
_private.Mathlib.Combinatorics.SetFamily.KruskalKatona.0.Finset.UV.familyMeasure : {n : ℕ} → Finset (Finset (Fin n)) → ℕ
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.upperBoundP?_eq_findP? : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x : α} {t : RBTree.RBSet α cmp} {cut : α → Ordering},
  t.findP? cut = some x → t.upperBoundP? cut = some x
-- Batteries.CodeAction.Misc
/-- Invoking tactic code action "Generate an explicit pattern match for 'induction'" in the
following:
```lean
example (x : Nat) : x = x := by
  induction x
```
produces:
```lean
example (x : Nat) : x = x := by
  induction x with
  | zero => sorry
  | succ n ih => sorry
```

It also works for `cases`.
 -/
Batteries.CodeAction.casesExpand : Batteries.CodeAction.TacticCodeAction
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.support_C_mul_X : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : MulSemiringAction (Multiplicative ℕ) R] {c : R},
  c ≠ 0 → (SkewPolynomial.C c * SkewPolynomial.X).support = {1}
-- Lean.Meta.Constructions.CtorElim
Lean.mkConstructorElimName : Lean.Name → Lean.Name → Lean.Name
-- Mathlib.Order.Hom.Set
/-- An order isomorphism between lattices induces an order isomorphism between corresponding
interval sublattices.  -/
OrderIso.Iic : {α : Type u_1} →
  {β : Type u_2} → [inst : Lattice α] → [inst_1 : Lattice β] → (e : α ≃o β) → (x : α) → ↑(Set.Iic x) ≃o ↑(Set.Iic (e x))
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.xPrevIsoSelf_comp_dTo_assoc : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {j : ι}
  (h : ¬c.Rel (c.prev j) j) {Z : V} (h_1 : C.X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (C.xPrevIsoSelf h).inv (CategoryTheory.CategoryStruct.comp (C.dTo j) h_1) =
    CategoryTheory.CategoryStruct.comp 0 h_1
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.isCoseparating_iff_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.ObjectProperty C)
  [inst_1 : ∀ (X : C), CategoryTheory.Limits.HasProduct (P.productToFamily X)],
  P.IsCoseparating ↔ ∀ (X : C), CategoryTheory.Mono (P.productTo X)
-- Mathlib.Probability.ProbabilityMassFunction.Monad
/-- The measure of a set under `pure a` is `1` for sets containing `a` and `0` otherwise.  -/
PMF.toMeasure_pure_apply : ∀ {α : Type u_1} (a : α) (s : Set α) [inst : MeasurableSpace α],
  MeasurableSet s → (PMF.pure a).toMeasure s = if a ∈ s then 1 else 0
-- Mathlib.Analysis.LocallyConvex.Separation
/-- If `s` and `t` are convex, `interior s` is nonempty and disjoint from `t`, then a continuous
`𝕜`-linear functional weakly separates `s` and `t`. If `t` is nonempty, this follows from
`geometric_hahn_banach_of_nonempty_interior`; if `t = ∅`, the zero functional works.  -/
RCLike.geometric_hahn_banach_of_nonempty_interior' : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E]
  {s t : Set E} [inst_3 : RCLike 𝕜] [inst_4 : Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E]
  [ContinuousSMul 𝕜 E],
  Convex ℝ s →
    Convex ℝ t →
      Disjoint (interior s) t →
        (interior s).Nonempty → ∃ f u, (∀ a ∈ s, RCLike.re (f a) ≤ u) ∧ ∀ b ∈ t, u ≤ RCLike.re (f b)