mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.HasGoodReduction.mk : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] {W : WeierstrassCurve K}
  [toIsMinimal : WeierstrassCurve.IsMinimal R W],
  (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W.Δ = 1 →
    WeierstrassCurve.HasGoodReduction R W
-- Mathlib.Topology.Bornology.Constructions
instBornologyAdditive : {α : Type u_1} → [Bornology α] → Bornology (Additive α)
-- Mathlib.Lean.Meta.CongrTheorems
Lean.Meta.instFastSubsingletonFinOfNatNat : Lean.Meta.FastSubsingleton (Fin 1)
-- Mathlib.CategoryTheory.Abelian.Images
CategoryTheory.Abelian.mono_factorThruImage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C}
  (f : P ⟶ Q) [inst_2 : CategoryTheory.Limits.HasCokernel f]
  [inst_3 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)] [CategoryTheory.Mono f],
  CategoryTheory.Mono (CategoryTheory.Abelian.factorThruImage f)
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.mul_of : ∀ {A : Type u_1} [inst : Monoid A] (a b : A), a * b = a * b
-- Lean.Elab.Do.Legacy
_private.Lean.Elab.Do.Legacy.0.Lean.Elab.Term.Do.varsToMessageData : Array Lean.Elab.Term.Do.Var → Lean.MessageData
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_eq_some_getKeyD : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a fallback : α}, a ∈ m → m.getKey? a = some (m.getKeyD a fallback)
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.Walk.ofBoxProdRight_boxProdRight : ∀ {α : Type u_1} {G : SimpleGraph α} [inst : DecidableEq α] [inst_1 : DecidableRel G.Adj] {a b₁ b₂ : α}
  (w : G.Walk b₁ b₂), (SimpleGraph.Walk.boxProdRight G a w).ofBoxProdRight = w
-- Mathlib.Analysis.Convex.Hull
convexHull_eq_empty : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s : Set E}, (convexHull 𝕜) s = ∅ ↔ s = ∅
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.congr_simp : ∀ (n : Type u) {inst : DecidableEq n} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (R : Type v) [inst_3 : CommRing R],
  Matrix.SpecialLinearGroup n R = Matrix.SpecialLinearGroup n R
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.leftOpRightOpEquiv_counitIso_hom_app_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : CategoryTheory.Functor C Dᵒᵖ) (X_1 : C),
  ((CategoryTheory.Functor.leftOpRightOpEquiv C D).counitIso.hom.app X).app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj X_1)
-- Init.Data.UInt.Lemmas
UInt8.ofInt_neg : ∀ (x : ℤ), UInt8.ofInt (-x) = -UInt8.ofInt x
-- Mathlib.Topology.GDelta.Basic
/-- A set `s` is closed and nowhere dense iff its complement `sᶜ` is open and dense.  -/
isClosed_isNowhereDense_iff_compl : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsClosed s ∧ IsNowhereDense s ↔ IsOpen sᶜ ∧ Dense sᶜ
-- Init.Data.Int.DivMod.Lemmas
Int.mul_sub_ediv_right : ∀ (a c : ℤ) {b : ℤ}, b ≠ 0 → (a * b - c) / b = a + -c / b
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instSub : {α : Type u_1} → [Sub α] → Sub (Colex α)
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.filterLinearMap.congr_simp : ∀ {ι : Type u} (γ : Type w) (β : ι → Type v) [inst : Semiring γ] [inst_1 : (i : ι) → AddCommMonoid (β i)]
  [inst_2 : (i : ι) → Module γ (β i)] (p p_1 : ι → Prop),
  p = p_1 →
    ∀ {inst_3 : DecidablePred p} [inst_4 : DecidablePred p_1],
      DFinsupp.filterLinearMap γ β p = DFinsupp.filterLinearMap γ β p_1
-- Init.Data.String.Lemmas.Length
String.length_eq_zero_iff : ∀ {s : String}, s.length = 0 ↔ s = ""
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toArray_mapM_eq_toArray_filterMapM : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n]
  [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_6 : MonadLiftT m n] [LawfulMonadLiftT m n]
  [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] {f : β → n γ} {it : Std.IterM m β},
  (Std.IterM.mapM f it).toArray = (Std.IterM.filterMapM (fun b => some <$> f b) it).toArray
-- Init.Data.Fin.Lemmas
/-- Version of `succ_one_eq_two` to be used by `dsimp`  -/
Fin.succ_one_eq_two : ∀ {n : ℕ}, Fin.succ 1 = 2
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.BoundedFormula.listDecode.eq_3 : ∀ {L : FirstOrder.Language} {α : Type u'} (n : ℕ) (R : L.Relations n) (k : ℕ)
  (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
  FirstOrder.Language.BoundedFormula.listDecode (Sum.inr (Sum.inl ⟨n, R⟩) :: Sum.inr (Sum.inr k) :: l) =
    (if h : ∀ (i : Fin n), (List.map Sum.getLeft? l)[i]?.join.isSome = true then
        if h' : ∀ (i : Fin n), ((List.map Sum.getLeft? l)[i]?.join.get ⋯).fst = k then
          ⟨k, FirstOrder.Language.BoundedFormula.rel R fun i => ⋯.mp ((List.map Sum.getLeft? l)[i]?.join.get ⋯).snd⟩
        else default
      else default) ::
      FirstOrder.Language.BoundedFormula.listDecode (List.drop n l)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey_erase_le_maxKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : t.erase k ≠ ∅}, (cmp ((t.erase k).maxKey he) (t.maxKey ⋯)).isLE = true
-- Mathlib.CategoryTheory.Functor.Category
/-- A natural transformation is a monomorphism if each component is.  -/
CategoryTheory.NatTrans.mono_of_mono_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : G ⟶ F) [∀ (X : C), CategoryTheory.Mono (α.app X)], CategoryTheory.Mono α
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
extChartAt_target : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (I : ModelWithCorners 𝕜 E H) [inst_5 : ChartedSpace H M] (x : M),
  (extChartAt I x).target = ↑I.symm ⁻¹' (chartAt H x).target ∩ Set.range ↑I
-- Init.Data.Rat.Lemmas
Rat.normalize_mul_left : ∀ {d : ℕ} {n : ℤ} {a : ℕ} (d0 : d ≠ 0) (a0 : a ≠ 0), Rat.normalize (↑a * n) (a * d) ⋯ = Rat.normalize n d d0
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.induction_on : ∀ {R : Type u} [inst : Semiring R] {motive : Polynomial R → Prop} (p : Polynomial R),
  (∀ (a : R), motive (Polynomial.C a)) →
    (∀ (p q : Polynomial R), motive p → motive q → motive (p + q)) →
      (∀ (n : ℕ) (a : R),
          motive (Polynomial.C a * Polynomial.X ^ n) → motive (Polynomial.C a * Polynomial.X ^ (n + 1))) →
        motive p
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.comp_tensor_id_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z : C}
  (f : W ⟶ X) (g : X ⟶ Y) {Z_1 : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f g)
        (CategoryTheory.CategoryStruct.id Z))
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.id Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom g (CategoryTheory.CategoryStruct.id Z)) h)
-- Mathlib.Topology.Homotopy.Lifting
Path.map'.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x y : X} (γ : Path x y)
  {f : X → Y} (h : ContinuousOn f (Set.range ⇑γ)),
  γ.map' h = { toFun := f ∘ ⇑γ, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.imp_trans : ∀ {σs : List (Type u)} {P Q R : Std.Do.SPred σs}, (P → Q) ∧ (Q → R) ⊢ₛ P → R
-- Init.Data.Fin.Lemmas
Fin.le_of_eq : ∀ {n : ℕ} {a b : Fin n}, a = b → a ≤ b
-- Mathlib.Order.Category.DistLat
DistLat.ofHom_apply : ∀ {X Y : Type u} [inst : DistribLattice X] [inst_1 : DistribLattice Y] (f : LatticeHom X Y) (x : X),
  (CategoryTheory.ConcreteCategory.hom (DistLat.ofHom f)) x = f x
-- Mathlib.Data.Sign.Defs
Left.sign_neg : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : Preorder α] [inst_2 : DecidableLT α] [AddLeftStrictMono α] (a : α),
  SignType.sign (-a) = -SignType.sign a
-- Init.Data.Range.Polymorphic.PRange
Std.Rio.instMembershipOfLT : {α : Type u} → [LT α] → Membership α (Std.Rio α)
-- Batteries.Data.BitVec.Lemmas
BitVec.toInt_ofFnBE : ∀ {n : ℕ} (f : Fin n → Bool), (BitVec.ofFnBE f).toInt = Int.ofBits (f ∘ Fin.rev)
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
/-- The (limit) cokernel cofork given by the composition
`P.complex.X 1 ⟶ P.complex.X 0 ⟶ Z` when `P : ProjectiveResolution Z`.  -/
CategoryTheory.ProjectiveResolution.cokernelCofork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {Z : C} → (P : CategoryTheory.ProjectiveResolution Z) → CategoryTheory.Limits.CokernelCofork (P.complex.d 1 0)
-- Mathlib.MeasureTheory.Integral.CircleIntegral
circleIntegral.integral_smul_const : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] (f : ℂ → ℂ) (a : E) (c : ℂ)
  (R : ℝ), ∮ (z : ℂ) in C(c, R), f z • a = (∮ (z : ℂ) in C(c, R), f z) • a
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.HasRightCalculusOfFractions.ext : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {W : CategoryTheory.MorphismProperty C}
  [self : W.HasRightCalculusOfFractions] ⦃X Y Y' : C⦄ (f₁ f₂ : X ⟶ Y) (s : Y ⟶ Y'),
  W s →
    CategoryTheory.CategoryStruct.comp f₁ s = CategoryTheory.CategoryStruct.comp f₂ s →
      ∃ X' t, ∃ (_ : W t), CategoryTheory.CategoryStruct.comp t f₁ = CategoryTheory.CategoryStruct.comp t f₂
-- Mathlib.Data.List.Map2
List.map₂Left'_nil_right : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : α → Option β → γ) (as : List α),
  List.map₂Left' f as [] = (List.map (fun a => f a none) as, [])
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.π_comp_H0Iso_hom_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : ↑(groupHomology.cycles A 0)),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.H0Iso A).hom)
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.π A 0)) x) =
    (Representation.Coinvariants.mk A.ρ) ((CategoryTheory.ConcreteCategory.hom (groupHomology.cyclesIso₀ A).hom) x)
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
circleMap.eq_1 : ∀ (c : ℂ) (R θ : ℝ), circleMap c R θ = c + ↑R * Complex.exp (↑θ * Complex.I)
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Gauss
/-- Given matrix `A`, solves the linear equation `A x = 0` and returns the solution as a tableau where
some variables are free and others (basic) variable are expressed as linear combinations of the free
ones.
 -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.Gauss.getTableau : {n m : ℕ} →
  {matType : ℕ → ℕ → Type} →
    [inst : Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] →
      matType n m → Lean.CoreM (Mathlib.Tactic.Linarith.SimplexAlgorithm.Tableau matType)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {l : List ((a : α) × β a)}
  {k : α} {fallback : β k},
  (List.map Sigma.fst l).contains k = false → (Std.DHashMap.Raw.ofList l).getD k fallback = fallback
-- Mathlib.Algebra.Group.Action.Faithful
/-- Two elements `g₁` and `g₂` are equal whenever they act in the same way on all points.  -/
FaithfulVAdd.eq_of_vadd_eq_vadd : ∀ {G : Type u_4} {P : Type u_5} {inst : VAdd G P} [self : FaithfulVAdd G P] {g₁ g₂ : G},
  (∀ (p : P), g₁ +ᵥ p = g₂ +ᵥ p) → g₁ = g₂
-- Mathlib.Algebra.Category.CommBialgCat
/-- Turn a morphism in `CommBialgCat` back into a `BialgHom`.  -/
CommBialgCat.Hom.hom : {R : Type u} → [inst : CommRing R] → {A B : CommBialgCat R} → A.Hom B → ↑A →ₐc[R] ↑B
-- Mathlib.Algebra.Lie.SerreConstruction
Matrix.instLieAlgebraToLieAlgebra : (R : Type u_1) →
  {B : Type u_2} →
    [inst : CommRing R] → (CM : Matrix B B ℤ) → [inst_1 : DecidableEq B] → LieAlgebra R (Matrix.ToLieAlgebra R CM)
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.addCore : {α β σ : Type} →
  Lean.Environment → Lean.ScopedEnvExtension α β σ → β → Lean.AttributeKind → Lean.Name → Lean.Environment
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.mem_carrier : ∀ {M : Type u_1} [inst : Mul M] {s : Subsemigroup M} {x : M}, x ∈ s.carrier ↔ x ∈ s
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
/-- A morphism `f` in `Arrow V` is sent to `0` in `RightFreyd V` if and only if there
exists a right homotopy between `f` and `0`.  -/
CategoryTheory.Preadditive.RightFreyd.quotient_map_eq_zero_iff : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v : CategoryTheory.Arrow V} (f : u ⟶ v),
  (CategoryTheory.Preadditive.RightFreyd.quotient V).map f = 0 ↔ Nonempty (CategoryTheory.Arrow.RightHomotopy f 0)
-- Lean.Expr
/-- Return `true` if `e` contains universe (aka `Level`) metavariables.
This is a constant time operation.
 -/
Lean.Expr.hasLevelMVar : Lean.Expr → Bool
-- Mathlib.Topology.Maps.Basic
Topology.IsQuotientMap.continuous_iff : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z],
  Topology.IsQuotientMap f → (Continuous g ↔ Continuous (g ∘ f))
-- Mathlib.SetTheory.Ordinal.Notation
ONote.cmp_compares : ∀ (a b : ONote) [a.NF] [b.NF], (a.cmp b).Compares a b
-- Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances
/-- The ring homomorphism `v.Completion →+* w.Completion` induced by `algebraMap K L`, when `w`
lies over `v`.  -/
NumberField.LiesOver.completionMap : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          {v : NumberField.InfinitePlace K} →
            {w : NumberField.InfinitePlace L} → [w.LiesOver v] → v.Completion →+* w.Completion
-- Mathlib.Analysis.Complex.PhragmenLindelof
/-- **Phragmen-Lindelöf principle** in the right half-plane. Let `f : ℂ → E` be a function such that

* `f` is differentiable in the open right half-plane and is continuous on its closure;
* `‖f z‖` is bounded from above by `A * exp(B * ‖z‖ ^ c)` on the open right half-plane
  for some `c < 2`;
* `‖f z‖` is bounded from above by a constant `C` on the imaginary axis;
* `‖f x‖` is bounded from above by a constant for large real values of `x`.

Then `‖f z‖` is bounded from above by `C` on the closed right half-plane.
See also `PhragmenLindelof.right_half_plane_of_tendsto_zero_on_real` for a weaker version.  -/
PhragmenLindelof.right_half_plane_of_bounded_on_real : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {C : ℝ} {f : ℂ → E} {z : ℂ},
  DiffContOnCl ℂ f {z | 0 < z.re} →
    (∃ c < 2, ∃ B, f =O[Bornology.cobounded ℂ ⊓ Filter.principal {z | 0 < z.re}] fun z => Real.exp (B * ‖z‖ ^ c)) →
      (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) Filter.atTop fun x => ‖f ↑x‖) →
        (∀ (x : ℝ), ‖f (↑x * Complex.I)‖ ≤ C) → 0 ≤ z.re → ‖f z‖ ≤ C
-- Mathlib.Algebra.Group.Indicator
/-- On non-dependent functions, `Set.indicator` on a singleton set equals `Pi.single`.  -/
Set.indicator_singleton : ∀ {ι : Type u_6} [inst : DecidableEq ι] {M : Type u_7} [inst_1 : Zero M] (i : ι) (f : ι → M),
  {i}.indicator f = Pi.single i (f i)
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.IsRestriction.exists_eq_delete : ∀ {α : Type u_1} {M N : Matroid α}, N.IsRestriction M → ∃ D ⊆ M.E, N = M.delete D
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.size_le_size_insertMany_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {l : List (α × β)}, m.size ≤ (Std.DHashMap.Raw.Const.insertMany m l).size
-- Init.Data.List.Find
List.get_find?_mem : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} (h : (List.find? p xs).isSome = true), (List.find? p xs).get h ∈ xs
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.IsAdmissible.singleton : ∀ {m a : ℕ}, a ≤ m → SimplexCategoryGenRel.IsAdmissible m [a]
-- Mathlib.Order.Category.OmegaCompletePartialOrder
/-- The pi-type gives a cone for a product.  -/
ωCPO.HasProducts.product : {J : Type v} → (f : J → ωCPO) → CategoryTheory.Limits.Fan f
-- Init.Data.List.Lemmas
List.mem_partition : ∀ {α : Type u_1} {l : List α} {a : α} {p : α → Bool}, a ∈ l ↔ a ∈ (List.partition p l).1 ∨ a ∈ (List.partition p l).2
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.zero_mk : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : ↥S), LocalizedModule.mk 0 s = 0
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- **Alias** of `AEMeasurable.sub`. -/
AEMeasurable.sub' : ∀ {G : Type u_2} {α : Type u_3} [inst : MeasurableSpace G] [inst_1 : Sub G] {m : MeasurableSpace α} {f g : α → G}
  {μ : MeasureTheory.Measure α} [MeasurableSub₂ G], AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (f - g) μ
-- Lean.Environment
/-- Function to transform state into data that should be imported into other modules. Returns entries
for all three olean levels at once so that expensive computations can be shared. When using the
module system without `import all`, `OLeanLevel.exported` is imported, else `OLeanLevel.private`.
Additionally, when using the module system in the language server, the `OLeanLevel.server` data is
accessible via `getModuleEntries (level := .server)`. By convention, each level should include all
data of previous levels.

This function is run once after elaborating the file and joining all asynchronous threads.
For non-module files, only the `private` field is used.
 -/
Lean.PersistentEnvExtension.exportEntriesFn : {α β σ : Type} → Lean.PersistentEnvExtension α β σ → Lean.Environment → σ → Lean.OLeanEntries (Array α)
-- Lean.Message
Lean.instInhabitedTraceResult : Inhabited Lean.TraceResult
-- Mathlib.Data.Bool.Basic
/-- `xor3 x y c` is `((x XOR y) XOR c)`.  -/
Bool.xor3 : Bool → Bool → Bool → Bool
-- Mathlib.Topology.Compactness.Compact
/-- If values of `f : Y → X` belong to a compact set `s` eventually along a filter `l`
and `s'` is the set of `MapClusterPt` for `f` along `l` in `s`,
then `f` tends to `𝓝ˢ s'` along `l`.  -/
IsCompact.tendsto_nhdsSet_of_mapClusterPt : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {Y : Type u_2} {l : Filter Y} {s' : Set X} {f : Y → X},
  IsCompact s → (∀ᶠ (x : Y) in l, f x ∈ s) → (∀ x ∈ s, MapClusterPt x l f → x ∈ s') → Filter.Tendsto f l (nhdsSet s')
-- Mathlib.Analysis.Normed.Order.Hom.Basic
AddGroupNormClass.toNormedAddGroup.eq_1 : ∀ {F : Type u_1} {α : Type u_2} [inst : FunLike F α ℝ] [inst_1 : AddGroup α] [inst_2 : AddGroupNormClass F α ℝ] (f : F),
  AddGroupNormClass.toNormedAddGroup f =
    { toNorm := (AddGroupSeminormClass.toSeminormedAddGroup f).toNorm,
      toAddGroup := (AddGroupSeminormClass.toSeminormedAddGroup f).toAddGroup,
      toPseudoMetricSpace := (AddGroupSeminormClass.toSeminormedAddGroup f).toPseudoMetricSpace,
      eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
-- Mathlib.RingTheory.Valuation.RankOne
/-- If a valuation has rank at most one and is non trivial,
then it has rank one  -/
Valuation.RankLeOne.rankOne_of_nontrivial : {Γ₀ : Type u_2} →
  [inst : LinearOrderedCommGroupWithZero Γ₀] →
    {K : Type u_3} →
      [inst_1 : DivisionRing K] →
        (v : Valuation K Γ₀) → [v.RankLeOne] → Nontrivial (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ → v.RankOne
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.AddAndFinalizeContext.vars : Lean.Elab.Command.AddAndFinalizeContext✝ → Array Lean.Expr
-- Mathlib.Analysis.Seminorm
/-- Closed balls at the origin are balanced.  -/
balanced_closedBall_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {r : ℝ}, Balanced 𝕜 (Metric.closedBall 0 r)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_insert' : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι],
  a ∉ s → (insert a s).sum = fun f => f a + ∑ x ∈ s, f x
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- Eta-expanded form of `MeasureTheory.StronglyMeasurable.div'` -/
MeasureTheory.StronglyMeasurable.fun_div' : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Div β]
  [ContinuousDiv β],
  MeasureTheory.StronglyMeasurable f →
    MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable fun i => f i / g i
-- Init.Data.UInt.Lemmas
UInt8.mul_zero : ∀ {a : UInt8}, a * 0 = 0
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trStmts₁.match_1.splitter : (motive : Turing.PartrecToTM2.Λ' → Sort u_1) →
  (x : Turing.PartrecToTM2.Λ') →
    ((p : Turing.PartrecToTM2.Γ' → Bool) →
        (k₁ k₂ : Turing.PartrecToTM2.K') →
          (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q)) →
      ((k : Turing.PartrecToTM2.K') →
          (s : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') →
            (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.push k s q)) →
        ((q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.read q)) →
          ((p : Turing.PartrecToTM2.Γ' → Bool) →
              (k : Turing.PartrecToTM2.K') →
                (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.clear p k q)) →
            ((q : Turing.PartrecToTM2.Λ') → motive q.copy) →
              ((q : Turing.PartrecToTM2.Λ') → motive q.succ) →
                ((q₁ q₂ : Turing.PartrecToTM2.Λ') → motive (q₁.pred q₂)) →
                  ((k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret k)) → motive x
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.instIsIsoMapTruncGEAppTruncGEπ : ∀ {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) [CategoryTheory.IsTriangulated C] (X : C) (n : ℤ),
  CategoryTheory.IsIso ((t.truncGE n).map ((t.truncGEπ n).app X))
-- Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties
CategoryTheory.Projective.instHasLiftingPropertyOfEpi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y P : C} (p : X ⟶ Y) [CategoryTheory.Epi p]
  [CategoryTheory.Projective P] [inst_3 : CategoryTheory.Limits.HasZeroObject C] (i : 0 ⟶ P),
  CategoryTheory.HasLiftingProperty i p
-- Init.Data.List.Perm
List.Perm.of_eq : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ = l₂ → l₁.Perm l₂
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.LeftExtension.coconeAtFunctor_map_hom : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (Y : D) {E E' : L.LeftExtension F} (φ : E ⟶ E'),
  ((CategoryTheory.Functor.LeftExtension.coconeAtFunctor L F Y).map φ).hom =
    (CategoryTheory.StructuredArrow.Hom.right φ).app Y
-- Mathlib.GroupTheory.OrderOfElement
card_zpowers_le : ∀ {G : Type u_1} [inst : Group G] [inst_1 : Fintype G] (a : G) {k : ℕ},
  k ≠ 0 → a ^ k = 1 → Fintype.card ↥(Subgroup.zpowers a) ≤ k