mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Congruence.Star
AddConGen.Rel.star : ∀ {A : Type u_1} [inst : AddMonoid A] [inst_1 : StarAddMonoid A] {r : A → A → Prop},
  (∀ (a b : A), r a b → r (star a) (star b)) → ∀ ⦃a b : A⦄, AddConGen.Rel r a b → AddConGen.Rel r (star a) (star b)
-- Mathlib.LinearAlgebra.Basis.Flag
Module.Basis.mem_toFlag : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {n : ℕ}
  (b : Module.Basis (Fin n) K V) {p : Submodule K V}, p ∈ b.toFlag ↔ ∃ k, b.flag k = p
-- Mathlib.GroupTheory.Coxeter.Matrix
/-- The Coxeter matrix of type Aₙ.

The corresponding Coxeter-Dynkin diagram is:
```
    o --- o --- o ⬝ ⬝ ⬝ ⬝ o --- o
```
 -/
CoxeterMatrix.A : (n : ℕ) → CoxeterMatrix (Fin n)
-- Mathlib.Topology.Order.Basic
isOpen_iff_generate_intervals : ∀ {α : Type u} [ts : TopologicalSpace α] [inst : Preorder α] [t : OrderTopology α] {s : Set α},
  IsOpen s ↔ TopologicalSpace.GenerateOpen {s | ∃ a, s = Set.Ioi a ∨ s = Set.Iio a} s
-- Init.Data.List.Lemmas
List.mem_dite_nil_right : ∀ {α : Type u_1} {p : Prop} {x : α} [inst : Decidable p] {l : p → List α},
  (x ∈ if h : p then l h else []) ↔ ∃ (h : p), x ∈ l h
-- Mathlib.Lean.Meta.CongrTheorems
Lean.Meta.instFastSubsingletonForallOfFastIsEmpty : ∀ {α : Sort u} [inst : Lean.Meta.FastIsEmpty α] {β : α → Sort v}, Lean.Meta.FastSubsingleton ((x : α) → β x)
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
/-- `ContinuousMultilinearMap.curryMid` as a linear isometry equivalence.  -/
ContinuousMultilinearMap.curryMidEquiv : (𝕜 : Type u) →
  {n : ℕ} →
    (Ei : Fin n.succ → Type wEi) →
      (G : Type wG) →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] →
            [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] →
              [inst_3 : NormedAddCommGroup G] →
                [inst_4 : NormedSpace 𝕜 G] →
                  (p : Fin (n + 1)) → ContinuousMultilinearMap 𝕜 Ei G ≃ₗᵢ[𝕜] Ei p →L[𝕜] Ei (p.succAbove i) [×n]→L[𝕜] G
-- Mathlib.Algebra.Star.StarAlgHom
/-- Turn an element of a type `F` satisfying `AlgEquivClass F R A B` and `StarHomClass F A B` into
an actual `StarAlgEquiv`. This is declared as the default coercion from `F` to `A ≃⋆ₐ[R] B`.  -/
StarAlgEquivClass.toStarAlgEquiv : {F : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : Add A] →
          [inst_1 : Mul A] →
            [inst_2 : SMul R A] →
              [inst_3 : Star A] →
                [inst_4 : Add B] →
                  [inst_5 : Mul B] →
                    [inst_6 : SMul R B] →
                      [inst_7 : Star B] →
                        [inst_8 : EquivLike F A B] →
                          [NonUnitalAlgEquivClass F R A B] → [StarHomClass F A B] → F → A ≃⋆ₐ[R] B
-- Aesop.Search.Expansion.Norm
Aesop.NormM.Context.mk.inj : ∀ {options : Aesop.Options'} {ruleSet : Aesop.LocalRuleSet} {normSimpContext : Aesop.NormSimpContext}
  {options_1 : Aesop.Options'} {ruleSet_1 : Aesop.LocalRuleSet} {normSimpContext_1 : Aesop.NormSimpContext},
  { options := options, ruleSet := ruleSet, normSimpContext := normSimpContext } =
      { options := options_1, ruleSet := ruleSet_1, normSimpContext := normSimpContext_1 } →
    options = options_1 ∧ ruleSet = ruleSet_1 ∧ normSimpContext = normSimpContext_1
-- Mathlib.Algebra.Group.Subsemigroup.Basic
Subsemigroup.mem_closure_of_mem : ∀ {M : Type u_1} [inst : Mul M] {s : Set M} {x : M}, x ∈ s → x ∈ Subsemigroup.closure s
-- Mathlib.Order.Filter.IsBounded
Filter.IsBoundedUnder.bddAbove_range : ∀ {β : Type u_2} [inst : Preorder β] [IsDirectedOrder β] {f : ℕ → β},
  Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) Filter.atTop f → BddAbove (Set.range f)
-- Init.Data.String.TakeDrop
/-- Removes trailing whitespace from a string by returning a slice whose end position is the last
non-whitespace character, or the start position if there is no non-whitespace character.

“Whitespace” is defined as characters for which `Char.isWhitespace` returns `true`.

Examples:

* `"abc".trimAsciiEnd == "abc".toSlice`

* `"   abc".trimAsciiEnd == "   abc".toSlice`

* `"abc \t  ".trimAsciiEnd == "abc".toSlice`

* `"  abc   ".trimAsciiEnd == "  abc".toSlice`

* `"abc\ndef\n".trimAsciiEnd == "abc\ndef".toSlice`
 -/
String.trimAsciiEnd : String → String.Slice
-- Mathlib.AlgebraicTopology.SimplicialSet.Subdivision
/-- The functor `SimplexCategory ⥤ SSet` which sends `⦋n⦌` to the nerve of the
partially ordered type of nonempty finite chains in `{0, ..., n}` (ulifted to `Type u`).
Vertices in `SimplexCategory.sd.obj ⦋n⦌` identify to nonempty subsets of `{0, ..., n}`.  -/
SimplexCategory.sd : CategoryTheory.Functor SimplexCategory SSet
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem_insert_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, (m.insert k v)[k] = v
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
/-- The compatibility of the shift functors on `CochainComplex C ℤ` with respect
to the addition of integers.  -/
CochainComplex.shiftFunctorAdd' : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (n₁ n₂ n₁₂ : ℤ) →
        n₁ + n₂ = n₁₂ →
          (CochainComplex.shiftFunctor C n₁₂ ≅
            (CochainComplex.shiftFunctor C n₁).comp (CochainComplex.shiftFunctor C n₂))
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.unop_s : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty Cᵒᵖ} {X Y : Cᵒᵖ}
  (φ : W.LeftFraction X Y), φ.unop.s = φ.s.unop
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- A subsemiring contains the semiring's 0.  -/
Subsemiring.zero_mem : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R), 0 ∈ s
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.Profunctor.op_obj_obj : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (P : CategoryTheory.Profunctor.{w, v₁, v₂, u₁, u₂} C D) (X : Dᵒᵖ) (Y : Cᵒᵖᵒᵖ),
  (P.op.obj X).obj Y = (P.obj (Opposite.unop (Opposite.unop Y))).obj X
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.card_type : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r], (Ordinal.type r).card = Cardinal.mk α
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.closure_singleton_natCast : ∀ {R : Type u} [inst : NonAssocRing R] (n : ℕ), Subring.closure {↑n} = ⊥
-- Mathlib.RingTheory.Support
Module.support_of_algebra : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_3} [inst_1 : Ring A] [inst_2 : Algebra R A],
  Module.support R A = PrimeSpectrum.zeroLocus ↑(RingHom.ker (algebraMap R A))
-- Mathlib.RingTheory.LocalProperties.Basic
RingHom.ofLocalizationSpanTarget_iff_finite : ∀ (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop),
  RingHom.OfLocalizationSpanTarget P ↔ RingHom.OfLocalizationFiniteSpanTarget P
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.toStructuredArrow'_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (d : D) (X : (CategoryTheory.CostructuredArrow F.op (Opposite.op d))ᵒᵖ),
  (CategoryTheory.CostructuredArrow.toStructuredArrow' F d).obj X =
    CategoryTheory.StructuredArrow.mk (Opposite.unop X).hom.unop
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Option.getD.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (opt : Option α) → ((x : α) → motive (some x)) → (Unit → motive none) → motive opt
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.ofSigmaCoforkFunctor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left}
  (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right}
  (a : CategoryTheory.Limits.Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)),
  (I.ofSigmaCoforkFunctor hc).obj a = CategoryTheory.Limits.Multicofork.ofSigmaCofork a
-- Init.Sym.Lemmas
Lean.Sym.String.lt_eq_false : ∀ (a b : String), decide (a < b) = false → (a < b) = False
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.pullFunctorIso_hom_app_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {p : S' ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'}
  {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)}
  (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = CategoryTheory.CategoryStruct.comp (f' j) p)
  {β : ι' → ι} {p'' : (j : ι') → X' j ⟶ X (β j)}
  (w' : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p'' j) (f (β j)) = CategoryTheory.CategoryStruct.comp (f' j) p)
  (X_1 : F.DescentData f) (i : ι'),
  ((CategoryTheory.Pseudofunctor.DescentData.pullFunctorIso F w w').hom.app X_1).hom i =
    X_1.hom (CategoryTheory.CategoryStruct.comp (p' i) (f (α i))) (p' i) (p'' i) ⋯ ⋯
-- Lean.Server.GoTo
Lean.Server.instFromJsonGoToKind.fromJson : Lean.Json → Except String Lean.Server.GoToKind
-- Init.Data.Range.Polymorphic.PRange
/-- The lower bound of the range. `lower` is not included in the range.
   -/
Std.Roo.lower : {α : Type u} → Std.Roo α → α
-- Mathlib.Order.Heyting.Basic
LE.le.codisjoint_hnot_right : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a b : α}, b ≤ a → Codisjoint a (￢b)
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.IsLocallyDirected.homOfLE_tAux_assoc : ∀ {J : Type w} [inst : CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme)
  [inst_1 : ∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)]
  [inst_2 : (F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] [inst_3 : Quiver.IsThin J] (i j : J) {k : J}
  (fi : k ⟶ i) (fj : k ⟶ j) {Z : AlgebraicGeometry.Scheme} (h : F.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.obj i).homOfLE ⋯)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.IsLocallyDirected.tAux F i j) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoOpensRange (F.map fi)).inv
      (CategoryTheory.CategoryStruct.comp (F.map fj) h)
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.isPrestackFor_ofArrows_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} {S : C}
  {X : ι → C} (f : (i : ι) → X i ⟶ S),
  F.IsPrestackFor (CategoryTheory.Presieve.ofArrows X f) ↔ Nonempty (F.toDescentData f).FullyFaithful
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.getEntryD : {α : Type u} → {β : α → Type v} → [BEq α] → α → (a : α) × β a → Std.DHashMap.Internal.AssocList α β → (a : α) × β a
-- Mathlib.Topology.LocallyConstant.Algebra
/-- `LocallyConstant.comap` as a linear map.  -/
LocallyConstant.comapₗ : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {Z : Type u_6} →
          (R : Type u_7) →
            [inst_2 : Semiring R] →
              [inst_3 : AddCommMonoid Z] →
                [inst_4 : Module R Z] → C(X, Y) → LocallyConstant Y Z →ₗ[R] LocallyConstant X Z
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.instInhabited.default : {s : String.Slice} → String.Slice.Pattern.ForwardSliceSearcher s
-- Mathlib.Algebra.Group.Units.Basic
LeftCancelMonoid.mul_eq_one : ∀ {α : Type u} [inst : LeftCancelMonoid α] [Subsingleton αˣ] {a b : α}, a * b = 1 ↔ a = 1 ∧ b = 1
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.zpow'_zero_of_ne_zero : ∀ {α : Type u_1} [inst : GroupWithZero α] {a : α}, a ≠ 0 → Mathlib.Tactic.FieldSimp.zpow' a 0 = 1
-- Mathlib.Order.Filter.Lift
Filter.lift_inf : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g h : Set α → Filter β},
  (f.lift fun x => g x ⊓ h x) = f.lift g ⊓ f.lift h
-- Mathlib.AlgebraicGeometry.Sites.EtalePoint
AlgebraicGeometry.Scheme.Cover.Over.congr_simp : ∀ (S : AlgebraicGeometry.Scheme) {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  [inst : P.IsStableUnderBaseChange] [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P]
  {X : AlgebraicGeometry.Scheme} [inst_2 : X.Over S]
  (𝒰 𝒰_1 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X),
  𝒰 = 𝒰_1 → AlgebraicGeometry.Scheme.Cover.Over S 𝒰 = AlgebraicGeometry.Scheme.Cover.Over S 𝒰_1
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.toCLM_neg : ∀ {𝕜₁ : 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] [inst_8 : IsTopologicalAddGroup F]
  {f : E →SWOT[σ] F}, (-f).toCLM = -f.toCLM
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.C_dvd_iff_dvd_coeff : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (r : R) (φ : MvPolynomial σ R),
  MvPolynomial.C r ∣ φ ↔ ∀ (i : σ →₀ ℕ), r ∣ MvPolynomial.coeff i φ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
ContDiffAt.ccosh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E} {n : WithTop ℕ∞},
  ContDiffAt ℂ n f x → ContDiffAt ℂ n (fun x => Complex.cosh (f x)) x
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
/-- **Alias** of the reverse direction of `Matrix.isElliptic_neg_iff`. -/
Matrix.IsElliptic.neg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Preorder R] {m : Matrix (Fin 2) (Fin 2) R},
  m.IsElliptic → (-m).IsElliptic
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.is_left_invariant_prehaar : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G},
  (interior U).Nonempty →
    ∀ (g : G) (K : TopologicalSpace.Compacts G),
      MeasureTheory.Measure.haar.prehaar (↑K₀) U (TopologicalSpace.Compacts.map (fun x => g * x) ⋯ K) =
        MeasureTheory.Measure.haar.prehaar (↑K₀) U K
-- Init.Data.Option.List
Option.foldl_toList : ∀ {β : Type u_1} {α : Type u_2} (o : Option β) (a : α) (f : α → β → α),
  List.foldl f a o.toList = o.elim a fun b => f a b
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.coe_equivMapOfInjective_apply : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (S : Subalgebra R A) (f : A →ₐ[R] B) (hf : Function.Injective ⇑f)
  (x : ↥S), ↑((S.equivMapOfInjective f hf) x) = f ↑x
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.d_f_comp_d_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (i₁ i₁' i₁'' : I₁) (i₂ : I₂), CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) ((K.d i₁' i₁'').f i₂) = 0
-- Mathlib.Algebra.Star.MonoidHom
StarMonoidHom.ext_iff : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Star A] [inst_2 : Monoid B] [inst_3 : Star B]
  {f g : A →⋆* B}, f = g ↔ ∀ (x : A), f x = g x
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- The topology of uniform convergence indeed gives the same notion of convergence as
`TendstoUniformly`.  -/
UniformFun.tendsto_iff_tendstoUniformly : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} {p : Filter ι} [inst : UniformSpace β] {F : ι → UniformFun α β}
  {f : UniformFun α β}, Filter.Tendsto F p (nhds f) ↔ TendstoUniformly (⇑UniformFun.toFun ∘ F) (UniformFun.toFun f) p
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.lift_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G]
  (X Y : LeftInvariantDerivation I G), ↑(X + Y) = ↑X + ↑Y
-- Mathlib.SetTheory.ZFC.PSet
PSet.nonempty_def : ∀ (u : PSet.{u_1}), u.Nonempty ↔ ∃ x, x ∈ u
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.insert.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (l' : Std.DTreeMap.Internal.Impl α β) →
      (motive : Std.DTreeMap.Internal.Impl.SizedBalancedTree α β l'.size (l'.size + 1) → Sort u_3) →
        (x : Std.DTreeMap.Internal.Impl.SizedBalancedTree α β l'.size (l'.size + 1)) →
          ((d : Std.DTreeMap.Internal.Impl α β) →
              (hd : d.Balanced) →
                (hd₁ : l'.size ≤ d.size) →
                  (hd₂ : d.size ≤ l'.size + 1) →
                    motive { impl := d, balanced_impl := hd, lb_le_size_impl := hd₁, size_impl_le_ub := hd₂ }) →
            motive x
-- Init.Data.List.Int.Sum
List.sum_div_length_le_max_of_max?_eq_some_int : ∀ {x : ℤ} {xs : List ℤ}, xs.max? = some x → xs.sum / ↑xs.length ≤ x
-- Mathlib.Order.Atoms
IsCoatom.lt_top : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, IsCoatom a → a < ⊤
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
_private.Mathlib.Geometry.Manifold.VectorField.LieBracket.0.VectorField.mfderiv_extChart_inverse_comp_aux : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] (x : M) (W : (x : M) → TangentSpace I x) [IsManifold I 2 M],
  ((mfderiv% ↑(extChartAt I x) x).inverse ∘SL
        (mfderiv[Set.range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) x)).inverse)
      (W (↑(extChartAt I x).symm (↑(extChartAt I x) x))) =
    W x
-- Mathlib.CategoryTheory.Sites.LocallyInjective
CategoryTheory.Presheaf.isLocallyInjective_of_injective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {FD : D → D → Type u_1} {CD : D → Type w} [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_3 : CategoryTheory.ConcreteCategory D FD] (J : CategoryTheory.GrothendieckTopology C)
  {F₁ F₂ : CategoryTheory.Functor Cᵒᵖ D} (φ : F₁ ⟶ F₂),
  (∀ (X : Cᵒᵖ), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (φ.app X))) →
    CategoryTheory.Presheaf.IsLocallyInjective J φ
-- Mathlib.Order.Filter.Partial
Function.graph.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Function.graph f = {(a, b) | f a = b}
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
PseudoMetricSpace.toEDist : {α : Type u} → [PseudoMetricSpace α] → EDist α
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_left_injOn₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : LinearOrder G₀] [PosMulStrictMono G₀] [MulPosMono G₀] {n : ℤ},
  n ≠ 0 → Set.InjOn (fun a => a ^ n) {a | 0 ≤ a}
-- Mathlib.Order.Heyting.Hom
/-- The proposition that a bi-Heyting homomorphism preserves the Heyting implication.  -/
BiheytingHomClass.map_himp : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} {inst : BiheytingAlgebra α} {inst_1 : BiheytingAlgebra β}
  {inst_2 : FunLike F α β} [self : BiheytingHomClass F α β] (f : F) (a b : α), f (a ⇨ b) = f a ⇨ f b
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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) (a b : ℤ) (h : a ≤ b) {Z : CategoryTheory.Functor C C}
  (h_1 : (t.truncLT b).comp (CategoryTheory.shiftFunctor C 1) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (t.truncGEδLT a)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (t.natTransTruncLTOfLE a b h) (CategoryTheory.shiftFunctor C 1)) h_1) =
    CategoryTheory.CategoryStruct.comp (t.natTransTruncGEOfLE a b h)
      (CategoryTheory.CategoryStruct.comp (t.truncGEδLT b) h_1)
-- Init.Data.List.Zip
List.head_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {f : α → β → γ}
  (h : List.zipWith f as bs ≠ []), (List.zipWith f as bs).head h = f (as.head ⋯) (bs.head ⋯)
-- Mathlib.NumberTheory.Real.Irrational
/-- If `x^n`, `n > 0`, is integer and is not the `n`-th power of an integer, then
`x` is irrational.  -/
irrational_nrt_of_notint_nrt : ∀ {x : ℝ} (n : ℕ) (m : ℤ), x ^ n = ↑m → (¬∃ y, x = ↑y) → 0 < n → Irrational x
-- Mathlib.RingTheory.Congruence.Hom
RingCon.comap_bot : ∀ {M : Type u_1} {N : Type u_2} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring N] (f : M →+* N),
  ⊥.comap f = RingCon.ker f
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ZeroExtend
Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend.go_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (w : ℕ) (input : aig.RefVec w)
  (newWidth curr : ℕ) (hcurr : curr ≤ newWidth) (s : aig.RefVec curr) (idx : ℕ) (h1 : idx < aig.decls.size)
  (h2 :
    idx < (Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend.go aig w input newWidth curr hcurr s).aig.decls.size),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend.go aig w input newWidth curr hcurr s).aig.decls[idx] =
    aig.decls[idx]
-- Mathlib.CategoryTheory.Functor.OfSequence
CategoryTheory.Functor.OfSequence.map.eq_def : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (x : ℕ → C) (x_1 : (n : ℕ) → x n ⟶ x (n + 1))
  (x_2 x_3 : ℕ),
  CategoryTheory.Functor.OfSequence.map x_1 x_2 x_3 =
    match (motive := (x : ℕ → C) → ((n : ℕ) → x n ⟶ x (n + 1)) → (x_5 x_6 : ℕ) → x_5 ≤ x_6 → (x x_5 ⟶ x x_6)) x, x_1,
      x_2, x_3 with
    | x, x_4, 0, 0 => fun x_5 => CategoryTheory.CategoryStruct.id (x 0)
    | x, f, 0, 1 => fun x => f 0
    | x, f, 0, l.succ => fun x_4 =>
      CategoryTheory.CategoryStruct.comp (f 0) (CategoryTheory.Functor.OfSequence.map (fun n => f (n + 1)) 0 l ⋯)
    | x, x_4, n.succ, 0 => fun a => nomatch a
    | x, f, k.succ, l.succ => fun x_4 => CategoryTheory.Functor.OfSequence.map (fun n => f (n + 1)) k l ⋯
-- Init.Data.Array.MapIdx
List.mapFinIdxM.go.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (as : List α)
  (f : (i : ℕ) → α → i < as.length → m β) (acc : Array β) (a : [].length + acc.size = as.length),
  List.mapFinIdxM.go as f [] acc a = pure acc.toList
-- Mathlib.Data.List.Pi
/-- `pi xs f` creates the list of functions `g` such that, for `x ∈ xs`, `g x ∈ f x`  -/
List.pi : {ι : Type u_1} →
  [DecidableEq ι] → {α : ι → Type u_2} → (l : List ι) → ((i : ι) → List (α i)) → List ((i : ι) → i ∈ l → α i)
-- Init.Data.UInt.Lemmas
UInt8.toBitVec_ofNat' : ∀ (n : ℕ), (UInt8.ofNat n).toBitVec = BitVec.ofNat 8 n
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.reorder.inj : ∀ {c c_1 : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr},
  Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.reorder c = Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.reorder c_1 →
    c = c_1