mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_insertMany_empty_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} [Std.TransOrd α] {l : List (α × β)} {k k' : α},
  compare k k' = Ordering.eq →
    ∀ {v : β},
      List.Pairwise (fun a b => ¬compare a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l →
          Std.DTreeMap.Internal.Impl.Const.get?
              (↑(Std.DTreeMap.Internal.Impl.Const.insertMany Std.DTreeMap.Internal.Impl.empty l ⋯)) k' =
            some v
-- Mathlib.AlgebraicTopology.SimplicialObject.II
SimplexCategory.II.monotone_map' : ∀ {n m : ℕ} (f : Fin (n + 1) →o Fin (m + 1)), Monotone (SimplexCategory.II.map' f)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : k ∉ t₂) {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂).get k h' = t₁.get k ⋯
-- Mathlib.CategoryTheory.Endomorphism
CategoryTheory.Aut.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {φ₁ φ₂ : CategoryTheory.Aut X},
  φ₁.hom = φ₂.hom → φ₁ = φ₂
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Injective.instSyzygies : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.EnoughInjectives C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y)
  [inst_3 : CategoryTheory.Limits.HasCokernel f], CategoryTheory.Injective (CategoryTheory.Injective.syzygies f)
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabOpen : Lean.Elab.Term.TermElab
-- Init.Data.SInt.Bitwise
Int64.not_not : ∀ {a : Int64}, ~~~~~~a = a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- Variant of `IsPullback.of_right` where `h₁₁` is induced from a morphism `h₁₃ : X₁₁ ⟶ X₁₃`, and
the universal property of the right square.

The objects fit in the following diagram:
```
X₁₁ - h₁₁ -> X₁₂ - h₁₂ -> X₁₃
|            |            |
v₁₁          v₁₂          v₁₃
↓            ↓            ↓
X₂₁ - h₂₁ -> X₂₂ - h₂₂ -> X₂₃
```
 -/
CategoryTheory.IsPullback.of_right' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₂ : X₁₂ ⟶ X₁₃}
  {h₂₁ : X₂₁ ⟶ X₂₂} {h₂₂ : X₂₂ ⟶ X₂₃} {h₁₃ : X₁₁ ⟶ X₁₃} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₃ ⟶ X₂₃}
  (s : CategoryTheory.IsPullback h₁₃ v₁₁ v₁₃ (CategoryTheory.CategoryStruct.comp h₂₁ h₂₂))
  (t : CategoryTheory.IsPullback h₁₂ v₁₂ v₁₃ h₂₂),
  CategoryTheory.IsPullback (t.lift h₁₃ (CategoryTheory.CategoryStruct.comp v₁₁ h₂₁) ⋯) v₁₁ v₁₂ h₂₁
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.instPartialOrder : {R : Type u} → [inst : NonUnitalNonAssocRing R] → PartialOrder (NonUnitalSubring R)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.map_add_toArray_rcc : ∀ {m n k : ℤ}, Array.map (fun x => x + k) (m...=n).toArray = ((m + k)...=n + k).toArray
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Fork.isLimitOfIsos.congr_simp : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {X' Y' : C}
  (c : CategoryTheory.Limits.Fork f g) (hc hc_1 : CategoryTheory.Limits.IsLimit c),
  hc = hc_1 →
    ∀ {f' g' : X' ⟶ Y'} (c' : CategoryTheory.Limits.Fork f' g') (e₀ e₀_1 : X ≅ X') (e_e₀ : e₀ = e₀_1) (e₁ e₁_1 : Y ≅ Y')
      (e_e₁ : e₁ = e₁_1) (e e_1 : c.pt ≅ c'.pt) (e_e : e = e_1)
      (comm₁ : CategoryTheory.CategoryStruct.comp e₀.hom f' = CategoryTheory.CategoryStruct.comp f e₁.hom)
      (comm₂ : CategoryTheory.CategoryStruct.comp e₀.hom g' = CategoryTheory.CategoryStruct.comp g e₁.hom)
      (comm₃ : CategoryTheory.CategoryStruct.comp e.hom c'.ι = CategoryTheory.CategoryStruct.comp c.ι e₀.hom),
      c.isLimitOfIsos hc c' e₀ e₁ e comm₁ comm₂ comm₃ = c.isLimitOfIsos hc_1 c' e₀_1 e₁_1 e_1 ⋯ ⋯ ⋯
-- Mathlib.Algebra.Group.TypeTags.Hom
/-- Reinterpret `α →* Multiplicative β` as `Additive α →+ β`.  -/
MonoidHom.toAdditiveLeft : {α : Type u_3} →
  {β : Type u_4} → [inst : MulOneClass α] → [inst_1 : AddZeroClass β] → (α →* Multiplicative β) ≃ (Additive α →+ β)
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.instInhabitedTrie : {a : Type} → Inhabited (Lean.Meta.LazyDiscrTree.Trie a)
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
/-- **Alias** of `thickenedIndicator_mono_infEDist`. -/
thickenedIndicator_mono_infEdist : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {δ : ℝ} (δ_pos : 0 < δ) {E : Set α} {x y : α},
  Metric.infEDist x E ≤ Metric.infEDist y E → (thickenedIndicator δ_pos E) y ≤ (thickenedIndicator δ_pos E) x
-- Mathlib.Analysis.Analytic.OfScalars
FormalMultilinearSeries.ofScalars_eq_zero : ∀ {𝕜 : Type u_1} (E : Type u_2) [inst : Field 𝕜] [inst_1 : Ring E] [inst_2 : Algebra 𝕜 E] [inst_3 : TopologicalSpace E]
  [inst_4 : IsTopologicalRing E] {c : ℕ → 𝕜} [Nontrivial E] (n : ℕ),
  FormalMultilinearSeries.ofScalars E c n = 0 ↔ c n = 0
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Mon.mul.go.match_1.eq_3 : ∀ (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Sort u_1) (pw₁ : Lean.Grind.CommRing.Power)
  (m₁ : Lean.Grind.CommRing.Mon) (pw₂ : Lean.Grind.CommRing.Power) (m₂ : Lean.Grind.CommRing.Mon)
  (h_1 : (m₁ : Lean.Grind.CommRing.Mon) → motive m₁ Lean.Grind.CommRing.Mon.unit)
  (h_2 : (m₂ : Lean.Grind.CommRing.Mon) → motive Lean.Grind.CommRing.Mon.unit m₂)
  (h_3 :
    (pw₁ : Lean.Grind.CommRing.Power) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (pw₂ : Lean.Grind.CommRing.Power) →
          (m₂ : Lean.Grind.CommRing.Mon) →
            motive (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂)),
  (match Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ with
    | m₁, Lean.Grind.CommRing.Mon.unit => h_1 m₁
    | Lean.Grind.CommRing.Mon.unit, m₂ => h_2 m₂
    | Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ => h_3 pw₁ m₁ pw₂ m₂) =
    h_3 pw₁ m₁ pw₂ m₂
-- Init.Data.Fin.Lemmas
Fin.castAdd_lt : ∀ {m : ℕ} (n : ℕ) (i : Fin m), ↑(Fin.castAdd n i) < m
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isLittleO_const_mul_right_iff : ∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] {S : Type u_17} [inst_1 : NormedRing S] [NormMulClass S] {f : α → E}
  {l : Filter α} {g : α → S} {c : S}, c ≠ 0 → ((f =o[l] fun x => c * g x) ↔ f =o[l] g)
-- Mathlib.RingTheory.PolynomialAlgebra
PolyEquivTensor.invFun.eq_1 : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (p : Polynomial A),
  PolyEquivTensor.invFun R A p = Polynomial.eval₂ (↑Algebra.TensorProduct.includeLeft) (1 ⊗ₜ[R] Polynomial.X) p
-- Init.GrindInstances.Ring.Fin
Lean.Grind.Fin.mul_one : ∀ {n : ℕ} [inst : NeZero n] (a : Fin n), a * 1 = a
-- Mathlib.Analysis.Calculus.ContDiff.Basic
contDiff_of_contDiffOn_union_of_isOpen : ∀ {𝕜 : 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] {s t : Set E} {f : E → F}
  {n : WithTop ℕ∞}, ContDiffOn 𝕜 n f s → ContDiffOn 𝕜 n f t → s ∪ t = Set.univ → IsOpen s → IsOpen t → ContDiff 𝕜 n f
-- Mathlib.Topology.Algebra.ProperAction.Basic
ProperSMul.mk : ∀ {G : Type u_1} {X : Type u_2} [inst : TopologicalSpace G] [inst_1 : TopologicalSpace X] [inst_2 : Group G]
  [inst_3 : MulAction G X], (IsProperMap fun gx => (gx.1 • gx.2, gx.2)) → ProperSMul G X
-- Lean.Meta.Tactic.Grind.Internalize
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.internalizeImpl.go.traverse : Lean.Expr → ℕ → Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Init.Data.Iterators.Combinators.Monadic.ULift
Std.Iterators.Types.ULiftIterator.mk.inj : ∀ {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u}
  {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ} {inner inner_1 : Std.IterM m β},
  { inner := inner } = { inner := inner_1 } → inner = inner_1
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- An object `Y` is terminal if for every `X` there is a unique morphism `X ⟶ Y`
(as an instance).  -/
CategoryTheory.Limits.IsTerminal.ofUnique : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (Y : C) → [h : (X : C) → Unique (X ⟶ Y)] → CategoryTheory.Limits.IsTerminal Y
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
/-- **Dirichlet Unit Theorem**. Any unit `x` of `𝓞 K` can be written uniquely as the product of
a root of unity and powers of the units of the fundamental system `fundSystem`.  -/
NumberField.Units.exist_unique_eq_mul_prod : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (x : (NumberField.RingOfIntegers K)ˣ),
  ∃! ζe, x = ↑ζe.1 * ∏ i, NumberField.Units.fundSystem K i ^ ζe.2 i
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- Note that as this lemma has an `if` in the statement, we include a `DecidableEq` argument.
This means you may not be able to `simp` using this lemma unless you `open scoped Classical`.  -/
CategoryTheory.Limits.biproduct.ι_π_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : DecidableEq J] (f : J → C)
  [inst_3 : CategoryTheory.Limits.HasBiproduct f] (j j' : J) {Z : C} (h : f j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j') h) =
    CategoryTheory.CategoryStruct.comp (if h : j = j' then CategoryTheory.eqToHom ⋯ else 0) h
-- Mathlib.Tactic.DuplicateDecls
/-- Return `true` if `cinfo` is defined as another constant.
If so, we assume that the declaration is intentionally duplicated.
This only works for exposed definitions.  -/
_private.Mathlib.Tactic.DuplicateDecls.0.Mathlib.Tactic.DuplicateDecls.isAlias : Lean.ConstantInfo → Bool
-- Mathlib.Data.Set.Order
/-- A function between linear orders which is neither monotone nor antitone makes a dent upright or
downright.  -/
Set.not_monotoneOn_not_antitoneOn_iff_exists_le_le : ∀ {α : Type u} {β : Type v} {s : Set α} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β},
  ¬MonotoneOn f s ∧ ¬AntitoneOn f s ↔
    ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- If `K` admits an orthogonal projection, `K` and `Kᗮ` are complements of each other.  -/
Submodule.isCompl_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [K.HasOrthogonalProjection], IsCompl K Kᗮ
-- Mathlib.Order.Extension.Well
instLinearOrderWellOrderExtensionOfWellFoundedLT : {α : Type u} → [inst : LT α] → [h : WellFoundedLT α] → LinearOrder (WellOrderExtension α)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
PresheafOfModules.ι_fromFreeYonedaCoproduct : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M : PresheafOfModules R) (m : M.Elements),
  CategoryTheory.CategoryStruct.comp (M.ιFreeYonedaCoproduct m) M.fromFreeYonedaCoproduct = m.fromFreeYoneda
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
MvPolynomial.eval₂Hom.eq_1 : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
  (g : σ → S₁),
  MvPolynomial.eval₂Hom f g =
    { toFun := MvPolynomial.eval₂ f g, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Init.Data.Int.DivMod.Basic
Int.negSucc_emod_negSucc : ∀ {a b : ℕ}, Int.negSucc a % Int.negSucc b = Int.subNatNat (b + 1) (a % (b + 1)).succ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.unitOfList_nil : ∀ {α : Type u} {cmp : α → α → Ordering}, Std.ExtTreeMap.unitOfList [] cmp = ∅
-- Batteries.Data.Array.Scan
Array.scanrM_empty : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} [inst : Monad m] {f : α → β → m β}
  {start stop : ℕ}, Array.scanrM f init #[] start stop = pure #[init]
-- Std.Sync.Channel
/-- Precondition: The channel must not be closed.
 -/
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.trySend' : {α : Type} → α → Std.AtomicT (Std.CloseableChannel.Bounded.State✝ α) BaseIO Bool
-- Init.Data.Array.Lemmas
Array.foldlM_loop_empty : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {s : ℕ} {h : s ≤ #[].size} [inst : Monad m] {f : β → α → m β}
  {init : β} {i j : ℕ}, Array.foldlM.loop f #[] s h i j init = pure init
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_top : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {l : ℕ} {v : α → M} {xs : Fin l → M},
  ⊤.Realize v xs ↔ True
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.mem_map : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] [inst_6 : Semiring B] [inst_7 : StarRing B]
  [inst_8 : Algebra R B] [inst_9 : StarModule R B] {S : StarSubalgebra R A} {f : A →⋆ₐ[R] B} {y : B},
  y ∈ StarSubalgebra.map f S ↔ ∃ x ∈ S, f x = y
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.ofClass_carrier : ∀ {S : Type u_6} {R : Type u_7} {A : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : StarRing R] [inst_4 : StarRing A] [inst_5 : StarModule R A] [inst_6 : SetLike S A]
  [inst_7 : SubsemiringClass S A] [inst_8 : SMulMemClass S R A] [inst_9 : StarMemClass S A] (s : S),
  ↑(StarSubalgebra.ofClass s) = ↑s
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.subtype_injective : ∀ {G : Type u_1} [inst : AddGroup G] (s : AddSubgroup G), Function.Injective ⇑s.subtype
-- Aesop.Tree.UnsafeQueue
Aesop.UnsafeQueue.instInhabited : Inhabited Aesop.UnsafeQueue
-- Mathlib.Data.Multiset.Find
Multiset.find?_eq_some_iff : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {a : α} {s : Multiset α} (hp : {x | x ∈ s ∧ p x}.Subsingleton),
  Multiset.find? p s hp = some a ↔ a ∈ s ∧ p a
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X₁ X₂ : C)
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂],
  (CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle X₁ X₂).inv.hom₂ =
    CategoryTheory.Limits.prod.lift CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd
-- Mathlib.Analysis.Meromorphic.Order
/-- The order of a sum is at least the minimum of the orders of the summands.
 -/
meromorphicOrderAt_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} {x : 𝕜},
  MeromorphicAt f₁ x →
    MeromorphicAt f₂ x → min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x) ≤ meromorphicOrderAt (f₁ + f₂) x
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The 1-cycles `Z₁(G, A)` of `A : Rep k G`, defined as the kernel of the map
`(G →₀ A) → A` defined by `single g a ↦ ρ_A(g⁻¹)(a) - a`.  -/
groupHomology.cycles₁ : {k G : Type u} → [inst : CommRing k] → [inst_1 : Group G] → (A : Rep.{u, u, u} k G) → Submodule k (G →₀ ↑A)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.toList_perm : ∀ {α : Type u} {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β}, m₁.Equiv m₂ → m₁.toList.Perm m₂.toList
-- Mathlib.GroupTheory.Perm.Finite
Equiv.Perm.perm_symm_on_of_perm_on_finset : ∀ {α : Type u} {s : Finset α} {f : Equiv.Perm α}, (∀ x ∈ s, f x ∈ s) → ∀ {y : α}, y ∈ s → (Equiv.symm f) y ∈ s
-- Mathlib.RingTheory.AdicCompletion.Completeness
AdicCompletion.restrictScalars_range_ofPowSMul_eq_ker_eval : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {n : ℕ}, Submodule.restrictScalars R (AdicCompletion.ofPowSMul I M n).range = (AdicCompletion.eval I M n).ker
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
String.Slice.Pattern.Model.ForwardSliceSearcher.toSearcher_of_isEmpty : ∀ {pat : String.Slice},
  pat.isEmpty = true →
    ∀ (s : String.Slice),
      String.Slice.Pattern.ToForwardSearcher.toSearcher pat s =
        { internalState := String.Slice.Pattern.ForwardSliceSearcher.emptyBefore s.startPos }
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_eq_some_getKey : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {a : α} {h' : Std.DTreeMap.Internal.Impl.contains a t = true}, t.getKey? a = some (t.getKey a h')
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_diff_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → Std.DHashMap.Raw.Const.get! (m₁.diff m₂) k = Std.DHashMap.Raw.Const.get! m₁ k
-- Mathlib.SetTheory.Ordinal.Notation
ONote.cmp.eq_4 : ∀ (e₁ : ONote) (n₁ : ℕ+) (a₁ e₂ : ONote) (n₂ : ℕ+) (a₂ : ONote),
  (e₁.oadd n₁ a₁).cmp (e₂.oadd n₂ a₂) = (e₁.cmp e₂).then ((cmp ↑n₁ ↑n₂).then (a₁.cmp a₂))
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `IsDedekindDomain.idealFactorsEquivOfQuotEquiv`.

---

The bijection between ideals of `R` dividing `I` and the ideals of `A` dividing `J` induced by
an isomorphism `f : R/I ≅ A/J`.  -/
idealFactorsEquivOfQuotEquiv : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing A] →
        [IsDedekindDomain A] →
          {I : Ideal R} → {J : Ideal A} → [IsDedekindDomain R] → R ⧸ I ≃+* A ⧸ J → ↑{p | p ∣ I} ≃o ↑{p | p ∣ J}
-- Mathlib.Algebra.Order.Ring.Ordering.Basic
RingPreordering.hasIdealSupport_of_isUnit_two : ∀ {R : Type u_1} [inst : CommRing R] {P : RingPreordering R}, IsUnit 2 → P.HasIdealSupport
-- Init.Data.Option.BasicAux
/-- Extracts the value from an `Option`, panicking on `none`.
 -/
Option.get! : {α : Type u} → [Inhabited α] → Option α → α
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
/-- The characteristic function of a measure is a product of
characteristic functions if and only if it is a product measure.
This is `charFunDual_eq_pi_iff` for `PiLp`.
See `charFun_eq_pi_iff` for the Hilbert space version.  -/
MeasureTheory.charFunDual_eq_pi_iff' : ∀ (p : ENNReal) [inst : Fact (1 ≤ p)] {ι : Type u_4} [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] {E : ι → Type u_5}
  [inst_3 : (i : ι) → NormedAddCommGroup (E i)] [inst_4 : (i : ι) → NormedSpace ℝ (E i)]
  {mE : (i : ι) → MeasurableSpace (E i)} [∀ (i : ι), BorelSpace (E i)] [∀ (i : ι), SecondCountableTopology (E i)]
  [∀ (i : ι), CompleteSpace (E i)] {μ : (i : ι) → MeasureTheory.Measure (E i)}
  {ν : MeasureTheory.Measure ((i : ι) → E i)} [∀ (i : ι), MeasureTheory.IsFiniteMeasure (μ i)]
  [MeasureTheory.IsFiniteMeasure ν],
  (∀ (L : StrongDual ℝ (WithLp p ((i : ι) → E i))),
      MeasureTheory.charFunDual (MeasureTheory.Measure.map (WithLp.toLp p) ν) L =
        ∏ i,
          MeasureTheory.charFunDual (μ i)
            (L ∘SL ↑(PiLp.continuousLinearEquiv p ℝ E).symm ∘SL ContinuousLinearMap.single ℝ E i)) ↔
    ν = MeasureTheory.Measure.pi μ
-- Aesop.ElabM
Aesop.ElabM.Context.mk.inj : ∀ {parsePriorities : Bool} {goal : Lean.MVarId} {parsePriorities_1 : Bool} {goal_1 : Lean.MVarId},
  { parsePriorities := parsePriorities, goal := goal } = { parsePriorities := parsePriorities_1, goal := goal_1 } →
    parsePriorities = parsePriorities_1 ∧ goal = goal_1
-- Mathlib.Data.Fin.Embedding
Fin.equivSubtype_symm_trans_valEmbedding : ∀ {n : ℕ}, Fin.equivSubtype.symm.toEmbedding.trans Fin.valEmbedding = Function.Embedding.subtype fun x => x < n
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
/-- Ring homomorphism between `A⟮b⟯` and `A⟮↑b⟯`.  -/
IntermediateField.RingHom.adjoinAlgebraMap : {A : Type u_3} →
  {B : Type u_4} →
    {C : Type u_5} →
      [inst : Field A] →
        [inst_1 : Field B] →
          [inst_2 : Field C] →
            [inst_3 : Algebra A B] →
              [inst_4 : Algebra B C] →
                [inst_5 : Algebra A C] → [IsScalarTower A B C] → (b : B) → ↥A⟮b⟯ →+* ↥A⟮(algebraMap B C) b⟯
-- Batteries.Util.ProofWanted
/-- Wrapper constant emitted in the placeholder, e.g. ``ProofWanted``.  -/
_private.Batteries.Util.ProofWanted.0.WantedCmdKind.wrapper : WantedCmdKind✝ → Lean.Name
-- Mathlib.Data.NNRat.Defs
NNRat.coe_min : ∀ (x y : ℚ≥0), ↑(min x y) = min ↑x ↑y
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn.isCompatible_zero_iff_true : ∀ {X : SSet} {i : Fin 2} (f : (j : Fin 2) → j ≠ i → (SSet.stdSimplex.obj { len := 0 } ⟶ X)),
  SSet.horn.IsCompatible f ↔ True
-- Mathlib.Analysis.Calculus.MeanValue
IsOpen.eqOn_of_deriv_eq : ∀ {𝕜 : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G] {s : Set 𝕜}
  {x : 𝕜} {f g : 𝕜 → G},
  IsOpen s →
    IsPreconnected s →
      DifferentiableOn 𝕜 f s →
        DifferentiableOn 𝕜 g s → Set.EqOn (deriv f) (deriv g) s → x ∈ s → f x = g x → Set.EqOn f g s
-- Init.Data.Array.Monadic
Array.filterMapM_unattach : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {P : α → Prop}
  {xs : Array (Subtype P)} {f : α → m (Option β)},
  Array.filterMapM f xs.unattach =
    Array.filterMapM
      (fun x =>
        match x with
        | ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (f (wfParam x))))
      xs
-- Mathlib.Order.Interval.Set.ProjIcc
Set.OrdConnected.IicExtend : ∀ {α : Type u_1} [inst : LinearOrder α] {b : α} {s : Set ↑(Set.Iic b)},
  s.OrdConnected → {x | Set.IicExtend (fun x => x ∈ s) x}.OrdConnected
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.liftTruncLE_aux : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {X Y : C} (f : X ⟶ Y) (n : ℤ) [t.IsLE X n],
  ∃ f', f = CategoryTheory.CategoryStruct.comp f' ((t.truncLEι n).app Y)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- The empty set has measure zero  -/
MeasureTheory.VectorMeasure.empty' : ∀ {α : Type u_3} [inst : MeasurableSpace α] {M : Type u_4} [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  (self : MeasureTheory.VectorMeasure α M), self.measureOf' ∅ = 0
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.trTape'.congr_simp : ∀ {Γ : Type u_1} {n : ℕ} {enc enc_1 : Γ → List.Vector Bool n} (e_enc : enc = enc_1) [inst : Inhabited Γ]
  (enc0 : enc default = List.Vector.replicate n false) (L L_1 : Turing.ListBlank Γ),
  L = L_1 → ∀ (R R_1 : Turing.ListBlank Γ), R = R_1 → Turing.TM1to1.trTape' enc0 L R = Turing.TM1to1.trTape' ⋯ L_1 R_1
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.pos_of_mem_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε : ℝ}, y ∈ Metric.ball x ε → 0 < ε
-- Mathlib.CategoryTheory.Sites.GlobalSections
/-- The global sections cone `Sheaf.coneΓ` is limiting - that is, global sections are limits even
when not all limits of shape `Cᵒᵖ` exist in `A`.  -/
CategoryTheory.Sheaf.isLimitConeΓ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {A : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
          [inst_2 : CategoryTheory.HasWeakSheafify J A] →
            [inst_3 : CategoryTheory.HasGlobalSectionsFunctor J A] →
              (F : CategoryTheory.Sheaf J A) → CategoryTheory.Limits.IsLimit F.coneΓ
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubmonoid.neg_mem_addUnits_iff : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) {x : AddUnits M}, -x ∈ S.addUnits ↔ x ∈ S.addUnits