mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.Trie
/-- A Trie is a key-value store where the keys are of type `String`,
and the internal structure is a tree that branches on the bytes of the string.   -/
Lean.Data.Trie : Type → Type
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.measure_neg : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : InvolutiveNeg G] [MeasurableNeg G] (μ : MeasureTheory.Measure G)
  [μ.IsNegInvariant] (A : Set G), μ (-A) = μ A
-- Mathlib.Tactic.NormNum.Irrational
/-- Proof of `k ^ n < m`.  -/
Mathlib.Meta.NormNum.NotPowerCertificate.pf_left : {m n : Q(ℕ)} → (self : Mathlib.Meta.NormNum.NotPowerCertificate m n) → Q(unknown_1 ^ «$n» < «$m»)
-- Mathlib.Algebra.Module.Congruence.Defs
/-- A `SMulCon` is closed under scalar multiplication.  -/
SMulCon.smul : ∀ {S : Type u_2} {M : Type u_3} [inst : SMul S M] (self : SMulCon S M) (s : S) {x y : M},
  self.toSetoid x y → self.toSetoid (s • x) (s • y)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.insertNthEquiv_zero : ∀ {n : ℕ} (α : Fin (n + 1) → Type u_3), Fin.insertNthEquiv α 0 = Fin.consEquiv α
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.map_le : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] (f : L →ₗ⁅R⁆ L') (I : LieIdeal R L) (J : LieIdeal R L'),
  LieIdeal.map f I ≤ J ↔ ⇑f '' ↑I ⊆ ↑J
-- Lean.Expr
/-- Annotate `e` with the LHS annotation. The delaborator displays
expressions of the form `lhs = rhs` as `lhs` when they have this annotation.
This is used to implement the infoview for the `conv` mode.

This version of `mkLHSGoal` does not check that the argument is an equality.
 -/
Lean.mkLHSGoalRaw : Lean.Expr → Lean.Expr
-- Mathlib.Algebra.Field.Rat
NNRat.inv_def : ∀ (q : ℚ≥0), q⁻¹ = NNRat.divNat q.den q.num
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.isInductiveFixpoint : Lean.Elab.PartialFixpointType → Bool
-- Mathlib.RingTheory.OrderOfVanishing.Basic
/-- If `x` is a non zero divisor, `ordMonoidWithZeroHom` is equal to the canonical embedding
of `Ring.ord R x` into `WithZero (Multiplicative ℤ)`.
 -/
Ring.ordMonoidWithZeroHom_eq_ord : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Nontrivial R] {x : R},
  x ∈ nonZeroDivisors R →
    (Ring.ordMonoidWithZeroHom R) x = ENat.recTopCoe 0 (fun x => ↑(Multiplicative.ofAdd ↑x)) (Ring.ord R x)
-- Mathlib.Computability.TuringMachine.Computable
/-- Each internal stack is finite.  -/
Turing.FinTM2.Γk₀Fin : (self : Turing.FinTM2) → Fintype (self.Γ self.k₀)
-- Mathlib.Data.EReal.Operations
EReal.add_sub_cancel_left : ∀ {a : EReal} {b : ℝ}, ↑b + a - ↑b = a
-- Init.Data.SInt.Lemmas
Int32.toNatClampNeg_ofIntTruncate_of_lt : ∀ {n : ℤ}, n < 2 ^ 31 → (Int32.ofIntClamp n).toNatClampNeg = n.toNat
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.domDomCongrLinearEquiv_symm_apply : ∀ (R : Type uR) (S : Type uS) (M₂ : Type v₂) (M₃ : Type v₃) [inst : Semiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : Module R M₂] [inst_3 : Semiring S] [inst_4 : AddCommMonoid M₃] [inst_5 : Module S M₃] [inst_6 : Module R M₃]
  [inst_7 : SMulCommClass R S M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ≃ ι₂) (a : MultilinearMap R (fun x => M₂) M₃),
  (MultilinearMap.domDomCongrLinearEquiv R S M₂ M₃ σ).symm a = (MultilinearMap.domDomCongrEquiv σ).invFun a
-- Mathlib.Data.Num.Lemmas
PosNum.size_eq_natSize : ∀ (n : PosNum), ↑n.size = n.natSize
-- Lean.Data.DeclarationRange
Lean.DeclarationRanges.mk.sizeOf_spec : ∀ (range selectionRange : Lean.DeclarationRange),
  sizeOf { range := range, selectionRange := selectionRange } = 1 + sizeOf range + sizeOf selectionRange
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.AtomNode.mk.sizeOf_spec : ∀ (vPos hPosSrc hPosTar : ℕ) (atom : Mathlib.Tactic.BicategoryLike.Atom),
  sizeOf { vPos := vPos, hPosSrc := hPosSrc, hPosTar := hPosTar, atom := atom } =
    1 + sizeOf vPos + sizeOf hPosSrc + sizeOf hPosTar + sizeOf atom
-- Mathlib.Order.Hom.Bounded
BotHom.instMax : {α : Type u_2} →
  {β : Type u_3} → [inst : Bot α] → [inst_1 : SemilatticeSup β] → [inst_2 : OrderBot β] → Max (BotHom α β)
-- Init.Data.List.Nat.Erase
List.getElem_eraseIdx_of_ge : ∀ {α : Type u_1} {l : List α} {i j : ℕ} (h : j < (l.eraseIdx i).length) (h' : i ≤ j), (l.eraseIdx i)[j] = l[j + 1]
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.coe_sInf : ∀ {α : Type u_1} [inst : CompleteLattice α] {L : CompleteSublattice α} (S : Set ↥L),
  ↑(sInf S) = sInf {x | ∃ s ∈ S, ↑s = x}
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.subsingleton : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [Subsingleton α], Subsingleton (Matrix m n α)
-- Init.PropLemmas
Decidable.iff_iff_and_or_not_and_not : ∀ {a b : Prop} [Decidable b], (a ↔ b) ↔ a ∧ b ∨ ¬a ∧ ¬b
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.instFintype : {q : ℕ} → [NeZero q] → Fintype (LucasLehmer.X q)
-- Mathlib.Algebra.Group.Defs
SubtractionMonoid.mk : {G : Type u} →
  [toSubNegMonoid : SubNegMonoid G] →
    (∀ (x : G), - -x = x) → (∀ (a b : G), -(a + b) = -b + -a) → (∀ (a b : G), a + b = 0 → -a = b) → SubtractionMonoid G
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.zeta_mul_pow_eq_sigma : ∀ {k : ℕ}, ArithmeticFunction.zeta * ArithmeticFunction.pow k = ArithmeticFunction.sigma k
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.prop_of_isLimit : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] [P.IsClosedUnderLimitsOfShape J] {F : CategoryTheory.Functor J C}
  {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c), (∀ (j : J), P (F.obj j)) → P c.pt
-- Mathlib.Tactic.Abel
/-- Specify whether we are in an additive commutative group or an additive commutative monoid.  -/
Mathlib.Tactic.Abel.Context.isGroup : Mathlib.Tactic.Abel.Context → Bool
-- Mathlib.Data.Fintype.Order
Finite.map_iInf_of_monotone : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder α]
  [inst_1 : ConditionallyCompleteLattice β] [Finite ι] [Nonempty ι] (f : ι → α) {g : α → β},
  Monotone g → g (⨅ i, f i) = ⨅ i, g (f i)
-- Mathlib.CategoryTheory.MorphismProperty.LocalEpi
CategoryTheory.ObjectProperty.localEpi_top_apply_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {f : X ⟶ Y},
  ⊤.localEpi f ↔ CategoryTheory.Epi f
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.prod.instSFinite : ∀ {α : Type u_4} {β : Type u_5} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ]
  {x_1 : MeasurableSpace β} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν], MeasureTheory.SFinite (μ.prod ν)
-- Mathlib.Algebra.Order.Group.Abs
mabs_le_max_mabs_mabs : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] {a b c : G},
  a ≤ b → b ≤ c → |b|ₘ ≤ max |a|ₘ |c|ₘ
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.mk'_mapId : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (S : CategoryTheory.StrictPseudofunctorCore B C) (x : B),
  (CategoryTheory.StrictPseudofunctor.mk' S).mapId x = CategoryTheory.eqToIso ⋯
-- Init.Prelude
instDecidableEqString : DecidableEq String
-- Init.Data.SInt.Lemmas
Int32.ofBitVec_lt_iff_slt : ∀ (a b : BitVec 32), Int32.ofBitVec a < Int32.ofBitVec b ↔ a.slt b = true
-- Lean.Linter.MissingDocs
Lean.Linter.linter.missingDocs : Lean.Option Bool
-- Mathlib.Geometry.Manifold.HasGroupoid
TopologicalSpace.Opens.chartAt_inclusion_symm_eventuallyEq : ∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  {U V : TopologicalSpace.Opens M} (hUV : U ≤ V) {x : ↥U},
  ↑(chartAt H
          (TopologicalSpace.Opens.inclusion hUV
            x)).symm =ᶠ[nhds (↑(chartAt H (TopologicalSpace.Opens.inclusion hUV x)) (Set.inclusion hUV x))]
    TopologicalSpace.Opens.inclusion hUV ∘ ↑(chartAt H x).symm
-- Init.Data.Nat.Lemmas
_private.Init.Data.Nat.Lemmas.0.Nat.allLTTR_loop_eq_true : ∀ {n : ℕ} {f : (i : ℕ) → i < n → Bool} (j : ℕ) (hj : j ≤ n),
  Nat.allLTTR.loop✝ n f j hj = true ↔ ∀ (i : ℕ), n - j ≤ i → ∀ (h : i < n), f i h = true
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeff_injective : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k], Function.Injective SkewMonoidAlgebra.coeff
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
/-- Geometric progressions of length three are preserved under semigroup homomorphisms.  -/
ThreeGPFree.image' : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {s : Set α}
  [inst_2 : FunLike F α β] [MulHomClass F α β] (f : F), Set.InjOn (⇑f) (s * s) → ThreeGPFree s → ThreeGPFree (⇑f '' s)
-- Mathlib.AlgebraicGeometry.EffectiveEpi
/-- If `π : X ⟶ Y` is surjective and flat between affine schemes, then any morphism `f : X ⟶ S` of
schemes whose two pullbacks to `X ×[Y] X` agree descends Zariski locally on `Y`: there exists an
open cover `𝒰` of `Y` such that for each `i` there is `u : 𝒰.X i ⟶ S` with
`pullback.fst π (𝒰.f i) ≫ f = pullback.snd π (𝒰.f i) ≫ u`.  -/
_private.Mathlib.AlgebraicGeometry.EffectiveEpi.0.AlgebraicGeometry.EffectiveEpiConstruction.exists_openCover_exists : ∀ {X Y S : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y] (π : X ⟶ Y)
  [AlgebraicGeometry.Surjective π] [AlgebraicGeometry.Flat π] (f : X ⟶ S),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst π π) f =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd π π) f →
    ∃ 𝒰,
      ∀ (i : 𝒰.I₀),
        ∃ u,
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst π (𝒰.f i)) f =
            CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd π (𝒰.f i)) u
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pushout.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f f_1 : X ⟶ Y) (e_f : f = f_1) (g g_1 : X ⟶ Z)
  (e_g : g = g_1) [inst_1 : CategoryTheory.Limits.HasPushout f g],
  CategoryTheory.Limits.pushout f g = CategoryTheory.Limits.pushout f_1 g_1
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.mopRingEquivOp_apply_coe : ∀ {R : Type u_2} [inst : NonAssocSemiring R] (S : Subsemiring R) (a : (↥S)ᵐᵒᵖ),
  ↑(S.mopRingEquivOp a) = MulOpposite.op ↑(MulOpposite.unop a)
-- Mathlib.Data.NNReal.Defs
NNReal.inv_le_of_le_mul : ∀ {r p : NNReal}, 1 ≤ r * p → r⁻¹ ≤ p
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.monoidalPi' : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] →
        {D : Type u_1} →
          [inst_2 : CategoryTheory.Category.{v_1, u_1} D] →
            [inst_3 : CategoryTheory.MonoidalCategory D] →
              (F : (i : I) → CategoryTheory.Functor D (C i)) →
                [(i : I) → (F i).Monoidal] → (CategoryTheory.Functor.pi' F).Monoidal
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
/-- **Alias** of the forward direction of `OpenPartialHomeomorph.IsImage.iff_preimage_eq'`. -/
OpenPartialHomeomorph.IsImage.preimage_eq' : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y},
  e.IsImage s t → e.source ∩ ↑e ⁻¹' (e.target ∩ t) = e.source ∩ s
-- Lean.Data.Lsp.Basic
Lean.Lsp.CreateFile.mk : Lean.Lsp.DocumentUri → Option Lean.Lsp.CreateFile.Options → Option String → Lean.Lsp.CreateFile
-- Mathlib.Analysis.Analytic.Constructions
/-- `AnalyticOn.comp` for functions on product spaces  -/
AnalyticOn.comp₂ : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5} {H : Type u_6}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : NormedAddCommGroup H] [inst_8 : NormedSpace 𝕜 H]
  {h : F × G → H} {f : E → F} {g : E → G} {s : Set (F × G)} {t : Set E},
  AnalyticOn 𝕜 h s →
    AnalyticOn 𝕜 f t → AnalyticOn 𝕜 g t → Set.MapsTo (fun y => (f y, g y)) t s → AnalyticOn 𝕜 (fun x => h (f x, g x)) t
-- Mathlib.Topology.Algebra.Group.Basic
AddGroup.continuousConstSMul_int : ∀ {A : Type u_1} [inst : AddGroup A] [inst_1 : TopologicalSpace A] [IsTopologicalAddGroup A], ContinuousConstSMul ℤ A
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.IsBase.cardinalMk_eq_cRank : ∀ {α : Type u} {M : Matroid α} {B : Set α} [M.InvariantCardinalRank], M.IsBase B → Cardinal.mk ↑B = M.cRank
-- Mathlib.Algebra.Homology.Single
ChainComplex.single₀_obj_zero : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] (A : V), ((ChainComplex.single₀ V).obj A).X 0 = A
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k k' : α} {f : Option β → Option β}, (t.alter k f)[k']? = if cmp k k' = Ordering.eq then f t[k]? else t[k']?
-- Mathlib.CategoryTheory.Join.Sum
CategoryTheory.Join.instEssSurjSumFromSum : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D], (CategoryTheory.Join.fromSum C D).EssSurj
-- Mathlib.RingTheory.Etale.Field
/-- If `A` is an essentially of finite type algebra over a field `K`, then `A` is formally étale
over `K` if and only if `A` is a finite product of separable field extensions.
 -/
Algebra.FormallyEtale.iff_exists_algEquiv_prod : ∀ (K : Type u_1) (A : Type u) [inst : Field K] [inst_1 : CommRing A] [inst_2 : Algebra K A] [Algebra.EssFiniteType K A],
  Algebra.FormallyEtale K A ↔ ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Algebra.IsSeparable K (Ai i)
-- Mathlib.NumberTheory.Ostrowski
_private.Mathlib.NumberTheory.Ostrowski.0.tendsto_const_rpow_inv : ∀ {C : ℝ}, 0 < C → Filter.Tendsto (fun k => C ^ (↑k)⁻¹) Filter.atTop (nhds 1)
-- Mathlib.MeasureTheory.MeasurableSpace.Invariants
MeasurableSpace.measurable_invariants_of_semiconj : ∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_2} [inst_1 : MeasurableSpace β] {fa : α → α} {fb : β → β}
  {g : α → β}, Measurable g → Function.Semiconj g fa fb → Measurable g
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.unmixedEmbeddingsOver.eq_1 : ∀ {K : Type u_3} (L : Type u_4) [inst : Field K] [inst_1 : Field L] (ψ : K →+* ℂ) [inst_2 : Algebra K L],
  NumberField.ComplexEmbedding.unmixedEmbeddingsOver L ψ =
    {φ | NumberField.ComplexEmbedding.LiesOver φ ψ ∧ NumberField.ComplexEmbedding.IsUnmixed K φ}
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.mod_opow_log_lt_self : ∀ (b : Ordinal.{u_1}) {o : Ordinal.{u_1}}, o ≠ 0 → o % b ^ Ordinal.log b o < o
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.Hom.w : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Under X} (φ : f ⟶ g),
  CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.Under.Hom.right φ) = g.hom
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithUpper.instTopologicalSpace : {α : Type u_1} → [Preorder α] → TopologicalSpace (Topology.WithUpper α)
-- Mathlib.Data.EReal.Inv
EReal.sign_top : SignType.sign ⊤ = 1
-- Lean.Meta.SizeOf
/-- Helper method for `mkMinorProof`. The proof step is one of the following
- Reflexivity
- Assumption (i.e., using an inductive hypotheses from `ys`)
- `mkSizeOfAuxLemma` application. This case happens when we have multiple levels of nesting
 -/
_private.Lean.Meta.SizeOf.0.Lean.Meta.SizeOfSpecNested.mkMinorProofStep : Array Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.SizeOfSpecNested.M Lean.Expr
-- Init.Data.Vector.Monadic
Vector.mapM_mk_empty : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {f : α → m β}, Vector.mapM f #v[] = pure #v[]
-- Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
ArithmeticFunction.vonMangoldt_mul_zeta : ArithmeticFunction.vonMangoldt * ↑ArithmeticFunction.zeta = ArithmeticFunction.log
-- Std.Data.ExtDHashMap.Lemmas
/-- Simpler variant of `getD_filter` when `LawfulBEq` is available.  -/
Std.ExtDHashMap.Const.getD_filter' : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : LawfulBEq α]
  {f : α → β → Bool} {k : α} {fallback : β},
  Std.ExtDHashMap.Const.getD (Std.ExtDHashMap.filter f m) k fallback =
    (Option.filter (f k) (Std.ExtDHashMap.Const.get? m k)).getD fallback
-- Mathlib.RingTheory.SimpleModule.Basic
IsSemisimpleModule.of_injective : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_5}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [IsSemisimpleModule R M] (f : N →ₗ[R] M),
  Function.Injective ⇑f → IsSemisimpleModule R N
-- Mathlib.SetTheory.Cardinal.HasCardinalLT
HasCardinalLT.eq_1 : ∀ (X : Type u) (κ : Cardinal.{v}), HasCardinalLT X κ = (Cardinal.lift.{v, u} (Cardinal.mk X) < Cardinal.lift.{u, v} κ)
-- Mathlib.FieldTheory.Galois.Basic
IntermediateField.restrictRestrictAlgEquivMapHom_surjective : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K L : IntermediateField F E)
  [inst_3 : Normal F ↥K] [FiniteDimensional F ↥K] [FiniteDimensional (↥L) E] [IsGalois (↥L) E],
  K ⊓ L = ⊥ → Function.Surjective ⇑(IntermediateField.restrictRestrictAlgEquivMapHom F (↥K) (↥L) E)
-- Mathlib.Tactic.LinearCombinationPrime
Mathlib.Tactic.LinearCombinationPrime.sub_pf : ∀ {α : Type u_1} {a₁ a₂ b₁ b₂ : α} [inst : Sub α], a₁ = b₁ → a₂ = b₂ → a₁ - a₂ = b₁ - b₂
-- Batteries.Lean.Meta.Basic
/-- Get the type the given metavariable after instantiating metavariables and cleaning up
annotations.  -/
Lean.MVarId.getTypeCleanup : Lean.MVarId → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Ring.Int.Parity
Int.coe_nat_two_pow_pred : ∀ (p : ℕ), ↑(2 ^ p - 1) = 2 ^ p - 1
-- Mathlib.Data.NNReal.Basic
NNReal.image_coe_uIoo : ∀ (x y : NNReal), NNReal.toReal '' Set.uIoo x y = Set.uIoo ↑x ↑y
-- Mathlib.Computability.Language
Language.mem_one : ∀ {α : Type u_1} (x : List α), x ∈ 1 ↔ x = []
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Iio : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {b : ι → α},
  Filter.Tendsto b l Filter.atTop → ∀ [NoMaxOrder α], MeasureTheory.AECover μ l fun i => Set.Iio (b i)
-- Mathlib.Analysis.Analytic.Composition
CPolynomialOn.comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {t : Set F} {g : F → G} {f : E → F},
  CPolynomialOn 𝕜 g t → CPolynomialOn 𝕜 f s → Set.MapsTo f s t → CPolynomialOn 𝕜 (g ∘ f) s
-- Lean.Parser.Extension
Lean.Parser.AliasValue.unary.injEq : ∀ {α : Type} (p p_1 : α → α), (Lean.Parser.AliasValue.unary p = Lean.Parser.AliasValue.unary p_1) = (p = p_1)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.lintegral_finsetSum : ∀ {α : Type u_1} {m : MeasurableSpace α} {ι : Type u_5} (f : MeasureTheory.SimpleFunc α ENNReal)
  (μ : ι → MeasureTheory.Measure α) (s : Finset ι), f.lintegral (∑ i ∈ s, μ i) = ∑ i ∈ s, f.lintegral (μ i)
-- Init.Data.Array.Lemmas
Array.mem_flatMap : ∀ {α : Type u_1} {β : Type u_2} {f : α → Array β} {b : β} {xs : Array α}, b ∈ Array.flatMap f xs ↔ ∃ a ∈ xs, b ∈ f a
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.brecOn_1.eq : ∀ {motive_1 : Lean.Elab.Term.Do.Code → Sort u}
  {motive_2 : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u}
  {motive_3 : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u}
  {motive_4 : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u}
  {motive_5 : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u}
  {motive_6 : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code → Sort u}
  {motive_7 : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code → Sort u}
  (t : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) (F_1 : (t : Lean.Elab.Term.Do.Code) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_1 t → motive_2 t)
  (F_3 : (t : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_2 t → motive_3 t)
  (F_4 : (t : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_3 t → motive_4 t)
  (F_5 : (t : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_4 t → motive_5 t)
  (F_6 : (t : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Lean.Elab.Term.Do.Code.below_5 t → motive_6 t)
  (F_7 : (t : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Lean.Elab.Term.Do.Code.below_6 t → motive_7 t),
  Lean.Elab.Term.Do.Code.brecOn_1 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 =
    F_2 t (Lean.Elab.Term.Do.Code.brecOn_1.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7).2
-- Mathlib.FieldTheory.IsRealClosed.Basic
IsRealClosed.exists_eq_pow_of_odd : ∀ {R : Type u} [inst : Field R] [IsRealClosed R] (x : R) {n : ℕ}, Odd n → ∃ r, x = r ^ n
-- Lean.Elab.DocString
Lean.Doc.DocArg.str.sizeOf_spec : ∀ (val : Lean.StrLit), sizeOf (Lean.Doc.DocArg.str val) = 1 + sizeOf val
-- Mathlib.Algebra.Tropical.Basic
Tropical.addLeftMono : ∀ {R : Type u} [inst : LinearOrder R], AddLeftMono (Tropical R)
-- Mathlib.Data.Rat.Cast.Order
NNRat.cast_max : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ≥0),
  ↑(max p q) = max ↑p ↑q
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_insert : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF →
    ∀ {k a fallback : α} {v : β k},
      (m.insert k v).getKeyD a fallback = if (k == a) = true then k else m.getKeyD a fallback
-- Mathlib.CategoryTheory.Adjunction.Parametrized
/-- a family of adjunctions  -/
CategoryTheory.ParametrizedAdjunction.adj : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} →
              {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} →
                (F ⊣₂ G) → (X₁ : C₁) → F.obj X₁ ⊣ G.obj (Opposite.op X₁)
-- Mathlib.Algebra.Algebra.Spectrum.Pi
Prod.quasispectrum_eq : ∀ {A : Type u_2} {B : Type u_3} {R : Type u_4} [inst : CommSemiring R] [inst_1 : NonUnitalRing A]
  [inst_2 : NonUnitalRing B] [inst_3 : Module R A] [inst_4 : Module R B] (a : A) (b : B),
  quasispectrum R (a, b) = quasispectrum R a ∪ quasispectrum R b
-- Mathlib.Logic.Equiv.Basic
/-- A subtype of a subtype is equivalent to the subtype of elements satisfying both predicates. This
version allows the “inner” predicate to depend on `h : p a`.  -/
Equiv.subtypeSubtypeEquivSubtypeExists : {α : Sort u_1} → (p : α → Prop) → (q : Subtype p → Prop) → Subtype q ≃ { a // ∃ (h : p a), q ⟨a, h⟩ }