mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.cokernelUnopOp_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {A B : Cᵒᵖ}
  (g : A ⟶ B),
  (CategoryTheory.cokernelUnopOp g).inv =
    (CategoryTheory.Limits.cokernel.desc g.unop (CategoryTheory.Limits.kernel.ι g).unop ⋯).op
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
/-- In an additive Lie group, inversion is a smooth map.  -/
contMDiff_neg : ∀ {𝕜 : 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) (n : WithTop ℕ∞)
  {G : Type u_4} [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G] [LieAddGroup I n G],
  ContMDiff I I n fun x => -x
-- Mathlib.Data.Ordmap.Ordset
Ordnode.insert_eq_insertWith : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DecidableLE α] (x : α) (t : Ordnode α),
  Ordnode.insert x t = Ordnode.insertWith (fun x_1 => x) x t
-- Mathlib.Algebra.Free
FreeAddMagma.pure_seq : ∀ {α β : Type u} {f : α → β} {x : FreeAddMagma α}, pure f <*> x = f <$> x
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
/-- If a set is not bounded below, its infimum is by convention `sInf ∅`.  -/
ConditionallyCompleteLinearOrder.csInf_of_not_bddBelow : ∀ {α : Type u_5} [self : ConditionallyCompleteLinearOrder α] (s : Set α), ¬BddBelow s → sInf s = sInf ∅
-- Init.Data.Nat.Bitwise.Basic
/-- Bitwise or. Usually accessed via the `|||` operator.

Each bit of the resulting value is set if the corresponding bit is set in at least one of the inputs.
 -/
Nat.lor : ℕ → ℕ → ℕ
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.ReflQuiv.forgetToQuiv.Faithful : CategoryTheory.ReflQuiv.forgetToQuiv.Faithful
-- Aesop.Tree.Data
Aesop.Goal.depth : Aesop.Goal → ℕ
-- Init.Data.BitVec.Lemmas
BitVec.toInt_extractLsb : ∀ {n hi lo : ℕ} {x : BitVec n}, (BitVec.extractLsb hi lo x).toInt = (↑(x.toNat >>> lo)).bmod (2 ^ (hi - lo + 1))
-- Mathlib.Tactic.Convert
Convert.ExpensiveConfig.toConfig : Convert.ExpensiveConfig → Congr!.Config
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.takeDTR.go.match_1.eq_1 : ∀ {α : Type u_1} (motive : ℕ → List α → Array α → Sort u_2) (n : ℕ) (x : α) (xs : List α) (acc : Array α)
  (h_1 : (n : ℕ) → (x : α) → (xs : List α) → (acc : Array α) → motive n.succ (x :: xs) acc)
  (h_2 : (x : List α) → (acc : Array α) → motive 0 x acc) (h_3 : (n : ℕ) → (acc : Array α) → motive n [] acc),
  (match n.succ, x :: xs, acc with
    | n.succ, x :: xs, acc => h_1 n x xs acc
    | 0, x, acc => h_2 x acc
    | n, [], acc => h_3 n acc) =
    h_1 n x xs acc
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Ioc_subset : ∀ {α : Type u_1} [inst : Preorder α] {p : α → Prop} (a b : { x // p x }), Subtype.val '' Set.Ioc a b ⊆ Set.Ioc ↑a ↑b
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.BirationalOver.symm : ∀ {S X Y : AlgebraicGeometry.Scheme} {sX : X ⟶ S} {sY : Y ⟶ S},
  AlgebraicGeometry.Scheme.BirationalOver sX sY → AlgebraicGeometry.Scheme.BirationalOver sY sX
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_eq_false_of_divCoeff : ∀ (ctx : Int.Internal.Linear.Context) (lhs rhs : Int.Internal.Linear.Expr) (k : ℤ),
  Int.Internal.Linear.unsatEqDivCoeffCert lhs rhs k = true →
    (Int.Internal.Linear.Expr.denote ctx lhs = Int.Internal.Linear.Expr.denote ctx rhs) = False
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_sin_mul_cos_sq : ∀ {a b : ℝ}, ∫ (x : ℝ) in a..b, Real.sin x * Real.cos x ^ 2 = (Real.cos a ^ 3 - Real.cos b ^ 3) / 3
-- Mathlib.Algebra.Group.Subsemigroup.Operations
MulHom.subsemigroupComap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (N' : Subsemigroup N),
  f.subsemigroupComap N' = { toFun := fun x => ⟨f ↑x, ⋯⟩, map_mul' := ⋯ }
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.sizeOfDiff : Std.HashSet ℕ → Std.HashSet ℕ → ℕ
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.mapComp_assoc_right : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h))
      (F.mapComp f (CategoryTheory.CategoryStruct.comp g h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (F.map h))
        (CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h)
          (F.map₂ (CategoryTheory.Bicategory.associator f g h).hom)))
-- Mathlib.Tactic.Module
/-- Basic meta-code "normal form" object of the `match_scalars` and `module` tactics: a type synonym
for a list of ordered triples comprising expressions representing terms of two types `R` and `M`
(where typically `M` is an `R`-module), together with a natural number "index".

The natural number represents the index of the `M` term in the `AtomM` monad: this is not enforced,
but is sometimes assumed in operations.  Thus when items `((a₁, x₁), k)` and `((a₂, x₂), k)`
appear in two different `Module.qNF` objects (i.e. with the same `ℕ`-index `k`), it is expected that
the expressions `x₁` and `x₂` are the same.  It is also expected that the items in a `Module.qNF`
list are in strictly increasing order by natural-number index.

By forgetting the natural number indices, an expression representing a `Mathlib.Tactic.Module.NF`
object can be built from a `Module.qNF` object; this construction is provided as
`Mathlib.Tactic.Module.qNF.toNF`.  -/
Mathlib.Tactic.Module.qNF : {u v : Lean.Level} → Q(Type u) → Q(Type v) → Type
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- The assertion that the short complex `S : ShortComplex C` is exact.  -/
CategoryTheory.ShortComplex.Exact : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → CategoryTheory.ShortComplex C → Prop
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.functorCategoryHasColimitsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasColimitsOfShape J C],
  CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.Functor K C)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.congrLeft_apply : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (R : Type u_10) {W : Type u_11} [inst_7 : Ring R]
  [inst_8 : AddCommGroup W] [inst_9 : Module k W] [inst_10 : Module R W] [inst_11 : SMulCommClass k R W]
  (e : P₁ ≃ᵃ[k] P₂) (Q : Type u_12) [inst_12 : AddTorsor W Q] (f : P₁ →ᵃ[k] Q) (x : P₂),
  ((AffineEquiv.congrLeft R e Q) f) x = f (e.symm x)
-- Mathlib.CategoryTheory.Limits.Final
/-- If a functor `R : D ⥤ C` is a right adjoint, it is final.  -/
CategoryTheory.Functor.final_of_adjunction : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (adj : L ⊣ R), R.Final
-- Mathlib.Topology.Order.Monotone
/-- **Alias** of `Monotone.countable_setOfPred_two_preimages`.

---

If a function is monotone in a second countable topological space, then there
are only countably many points that have several preimages.  -/
Monotone.countable_setOf_two_preimages : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] {f : α → β} [SecondCountableTopology α],
  Monotone f → {c | ∃ x y, x < y ∧ f x = c ∧ f y = c}.Countable
-- Mathlib.Probability.Moments.ComplexMGF
ProbabilityTheory.complexMGF_id_mul_I : ∀ {μ : MeasureTheory.Measure ℝ} (t : ℝ), ProbabilityTheory.complexMGF id μ (↑t * Complex.I) = MeasureTheory.charFun μ t
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.minView.match_3.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (r : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (l : Std.DTreeMap.Internal.Impl α β) →
      l.Balanced → Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size → Sort u_3)
  (hl : Std.DTreeMap.Internal.Impl.leaf.Balanced)
  (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot Std.DTreeMap.Internal.Impl.leaf.size r.size)
  (h_1 :
    (hl : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot Std.DTreeMap.Internal.Impl.leaf.size r.size) →
        motive Std.DTreeMap.Internal.Impl.leaf hl hlr)
  (h_2 :
    (size : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l' r' : Std.DTreeMap.Internal.Impl α β) →
            (hl : (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').Balanced) →
              (hlr :
                  Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').size
                    r.size) →
                motive (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') hl hlr),
  (match Std.DTreeMap.Internal.Impl.leaf, hl, hlr with
    | Std.DTreeMap.Internal.Impl.leaf, hl, hlr => h_1 hl hlr
    | Std.DTreeMap.Internal.Impl.inner size k' v' l' r', hl, hlr => h_2 size k' v' l' r' hl hlr) =
    h_1 hl hlr
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
SimpleGraph.singletonFinsubgraph_le_adj_right : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {e : G.Adj u v},
  SimpleGraph.singletonFinsubgraph v ≤ SimpleGraph.finsubgraphOfAdj e
-- Mathlib.Algebra.Order.Monovary
Monovary.div_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : CommGroup β] [inst_2 : LinearOrder β]
  [IsOrderedMonoid β] {f : ι → α} {g₁ g₂ : ι → β}, Monovary f g₁ → Antivary f g₂ → Monovary f (g₁ / g₂)
-- Mathlib.Analysis.Matrix.Order
Matrix.PosSemidef.posDef_iff_det_ne_zero : ∀ {𝕜 : Type u_1} {n : Type u_2} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : Matrix n n 𝕜},
  A.PosSemidef → (A.PosDef ↔ A.det ≠ 0)
-- Mathlib.Algebra.Homology.SingleHomology
/-- The canonical isomorphism `((single C c j).obj A).opcycles j ≅ A`  -/
HomologicalComplex.singleObjOpcyclesSelfIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        {ι : Type u_1} →
          [inst_3 : DecidableEq ι] →
            (c : ComplexShape ι) → (j : ι) → (A : C) → A ≅ ((HomologicalComplex.single C c j).obj A).opcycles j
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.pentagon_hom_inv_inv_inv_hom_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e)
  {Z : a ⟶ e}
  (h_1 :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))
        i ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).inv)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).inv h_1)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).hom i) h_1)
-- Mathlib.Data.Complex.Basic
/-- The "real part" map, considered as an additive group homomorphism.  -/
Complex.reAddGroupHom : ℂ →+ ℝ
-- Mathlib.Algebra.Order.GroupWithZero.Action.Synonym
Lex.instDistribMulAction : {G₀ : Type u_1} →
  {M₀ : Type u_2} →
    [inst : Monoid G₀] → [inst_1 : AddMonoid M₀] → [DistribMulAction G₀ M₀] → DistribMulAction (Lex G₀) M₀
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality
ContinuousCohomology.cochainsMap_f_hom : ∀ {k : Type u} {G H : Type v} [inst : Ring k] [inst_1 : TopologicalSpace k] [inst_2 : Group G]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] [inst_5 : Group H] [inst_6 : TopologicalSpace H]
  [inst_7 : IsTopologicalGroup H] {X : TopRep k G} {Y : TopRep k H} (φ : H →ₜ* G) (f : TopRep.res (↑φ) X ⟶ Y) (i : ℕ),
  TopModuleCat.Hom.hom ((ContinuousCohomology.cochainsMap φ f).f i) =
    ContIntertwiningMap.mapInvariantsOfRes (↑φ) (TopRep.Hom.hom (ContinuousCohomology.resolutionMap φ f (i + 1)))
-- Init.Data.String.Iterator
String.Iterator.curr : String.Legacy.Iterator → Char
-- Mathlib.Algebra.Ring.Equiv
/-- Transitivity of `RingEquiv`.  -/
RingEquiv.trans : {R : Type u_4} →
  {S : Type u_5} →
    {S' : Type u_6} →
      [inst : Mul R] →
        [inst_1 : Mul S] →
          [inst_2 : Add R] → [inst_3 : Add S] → [inst_4 : Mul S'] → [inst_5 : Add S'] → R ≃+* S → S ≃+* S' → R ≃+* S'
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.awayι_toSpecZero_assoc : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A) {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.Spec (CommRingCat.of ↥(𝒜 0)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.toSpecZero 𝒜) h) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.fromZeroRingHom 𝒜 (Submonoid.powers f))))
      h
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
WeakFEPair.hε : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (self : WeakFEPair E), self.ε ≠ 0
-- Mathlib.Tactic.DepRewrite
/-- Which transparency level to use when unifying the rewrite rule's LHS
against subterms of the term being rewritten.  -/
Mathlib.Tactic.DepRewrite.Config.transparency : Mathlib.Tactic.DepRewrite.Config → Lean.Meta.TransparencyMode
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.Equiv.beq_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap α (fun x => β) cmp} [inst : BEq β]
  [Std.TransCmp cmp] {m₃ m₄ : Std.DTreeMap α (fun x => β) cmp},
  m₁.Equiv m₃ → m₂.Equiv m₄ → Std.DTreeMap.Const.beq m₁ m₂ = Std.DTreeMap.Const.beq m₃ m₄
-- Lean.Data.Lsp.Communication
Lean.IO.FS.Stream.writeSerializedLspMessage : IO.FS.Stream → String → IO Unit
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.minEntry?.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) (size : ℕ) (k : α) (v : β k)
  (r : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α β) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)),
  (match Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r => h_2 size k v r
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1 =>
      h_3 size k v l size_1 k_1 v_1 l_1 r h r_1) =
    h_2 size k v r
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_eq_false_iff_exists_contains_eq_true : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → (m.isEmpty = false ↔ ∃ a, m.contains a = true)
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
/-- If the coefficient space is T2, then the multivariate power series is `tsum` of its monomials  -/
MvPowerSeries.WithPiTopology.as_tsum : ∀ {σ : Type u_1} {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : Semiring R] [T2Space R] (f : MvPowerSeries σ R),
  f = ∑' (d : σ →₀ ℕ), (MvPowerSeries.monomial d) ((MvPowerSeries.coeff d) f)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
/-- If `K` is a field with `F ⊆ K` and `S ⊆ K` then `adjoin F S ≤ K`.  -/
IntermediateField.adjoin_le_subfield : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Set E) {K : Subfield E},
  Set.range ⇑(algebraMap F E) ⊆ ↑K → S ⊆ ↑K → (IntermediateField.adjoin F S).toSubfield ≤ K
-- Mathlib.LinearAlgebra.Dimension.Free
/-- See also `finrank_eq_one_iff`  -/
Module.nonempty_linearEquiv_iff_finrank_eq_one : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  [StrongRankCondition R], Nonempty (R ≃ₗ[R] M) ↔ Module.finrank R M = 1
-- Aesop.Util.Tactic
_private.Aesop.Util.Tactic.0.Aesop.introsUnfolding.run : Lean.MVarId → Array Lean.FVarId → Lean.MetaM (Array Lean.FVarId × Lean.MVarId)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.mem_sInf_iff : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (p : P) (t : Set (AffineSubspace k P)), p ∈ sInf t ↔ ∀ s ∈ t, p ∈ s
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.inv_weightMap : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι₂ : Type u_8} {M₂ : Type u_9} {N₂ : Type u_10}
  [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂] [inst_7 : AddCommGroup N₂] [inst_8 : Module R N₂]
  (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (f : P.Equiv Q),
  (↑(RootPairing.Equiv.symm P Q f)).weightMap = ↑(RootPairing.Equiv.weightEquiv P Q f).symm
-- Init.Data.UInt.Bitwise
USize.toUInt32_shiftLeft_mod : ∀ (a b : USize), (a <<< (b % 32)).toUInt32 = a.toUInt32 <<< b.toUInt32
-- Mathlib.Analysis.Calculus.Deriv.Slope
/-- If a monotone function has a derivative within a set at a non-isolated point, then this
derivative is nonnegative.  -/
HasDerivWithinAt.nonneg_of_monotoneOn : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [OrderTopology 𝕜] {g : 𝕜 → 𝕜} {g' : 𝕜},
  AccPt x (Filter.principal s) → HasDerivWithinAt g g' s x → MonotoneOn g s → 0 ≤ g'
-- Mathlib.Order.PiLex
Pi.ofColex_apply : ∀ {ι : Type u_1} {β : ι → Type u_2} (x : Colex ((i : ι) → β i)) (i : ι), ofColex x i = x i
-- Init.Data.String.Defs
/-- The start position of `s`, as an `s.Pos`.  -/
String.Slice.startPos : (s : String.Slice) → s.Pos
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Adding the second vector passed to `oangle` to the first vector does not change the sign of
the angle.  -/
Orientation.oangle_sign_add_left : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V), (o.oangle (x + y) y).sign = (o.oangle x y).sign
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.injective_toEmbedding : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N],
  Function.Injective FirstOrder.Language.Equiv.toEmbedding
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.forIn_eq_forIn : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} {δ : Type w} {m' : Type w → Type w'} [inst : Monad m']
  [LawfulMonad m'] {f : α → β → δ → m' (ForInStep δ)} {init : δ},
  Std.HashMap.Raw.forIn f init m = forIn m init fun a d => f a.1 a.2 d
-- Mathlib.CategoryTheory.Action.Monoidal
/-- Given `X : Action (Type u) G` for `G` a group, then `G × X` (with `G` acting as left
multiplication on the first factor and by `X.ρ` on the second) is isomorphic as a `G`-set to
`G × X` (with `G` acting as left multiplication on the first factor and trivially on the second).
The isomorphism is given by `(g, x) ↦ (g, g⁻¹ • x)`.  -/
Action.leftRegularTensorIso : (G : Type u) →
  [inst : Group G] →
    (X : Action (Type u) G) →
      CategoryTheory.MonoidalCategoryStruct.tensorObj (Action.leftRegular G) X ≅
        CategoryTheory.MonoidalCategoryStruct.tensorObj (Action.leftRegular G) (Action.trivial G X.V)
-- Lean.DocString.Parser
/-- Parses a block command.
 -/
Lean.Doc.Parser.block_command : Lean.Doc.Parser.BlockCtxt → Lean.Parser.ParserFn
-- Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapComp : ∀ {a b c : CategoryTheory.LocallyDiscrete CommRingCatᵒᵖ} (x : a ⟶ b) (x_1 : b ⟶ c),
  CommRingCat.moduleCatRestrictScalarsPseudofunctor.mapComp x x_1 =
    CategoryTheory.Cat.Hom.isoMk
      (ModuleCat.restrictScalarsComp (CommRingCat.Hom.hom x_1.as.unop) (CommRingCat.Hom.hom x.as.unop))
-- Mathlib.Tactic.Simps.Basic
Simps.ProjectionRule.rename.inj : ∀ {oldName : Lean.Name} {oldStx : Lean.Syntax} {newName : Lean.Name} {newStx : Lean.Syntax} {oldName_1 : Lean.Name}
  {oldStx_1 : Lean.Syntax} {newName_1 : Lean.Name} {newStx_1 : Lean.Syntax},
  Simps.ProjectionRule.rename oldName oldStx newName newStx =
      Simps.ProjectionRule.rename oldName_1 oldStx_1 newName_1 newStx_1 →
    oldName = oldName_1 ∧ oldStx = oldStx_1 ∧ newName = newName_1 ∧ newStx = newStx_1
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitSource.mbtc.sizeOf_spec : ∀ (a b : Lean.Expr) (i : ℕ), sizeOf (Lean.Meta.Grind.SplitSource.mbtc a b i) = 1 + sizeOf a + sizeOf b + sizeOf i
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
/-- Recursor for `Fix F`  -/
MvQPF.Fix.rec : {n : ℕ} →
  {F : TypeVec.{u} (n + 1) → Type u} →
    [q : MvQPF F] → {α : TypeVec.{u} n} → {β : Type u} → (F (α ::: β) → β) → MvQPF.Fix F α → β
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopicRel.comp_continuousMap : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {S : Set X} ⦃f₀ f₁ : C(X, Y)⦄,
  f₀.HomotopicRel f₁ S → ∀ (g : C(Y, Z)), (g.comp f₀).HomotopicRel (g.comp f₁) S
-- Lean.Meta.Tactic.Symm
/-- Given a term `e : a ~ b`, construct a term in `b ~ a` using `@[symm]` lemmas.  -/
Lean.Expr.applySymm : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Data.List.Duplicate
List.Duplicate.below.cons_mem : ∀ {α : Type u_1} {x : α} {motive : (a : List α) → List.Duplicate x a → Prop} {l : List α} (a : x ∈ l),
  List.Duplicate.below ⋯
-- Lean.Meta.Basic
Lean.Meta.SynthInstanceCacheKey.mk.sizeOf_spec : ∀ (localInsts : Lean.LocalInstances) (type : Lean.Expr) (synthPendingDepth : ℕ),
  sizeOf { localInsts := localInsts, type := type, synthPendingDepth := synthPendingDepth } =
    1 + sizeOf localInsts + sizeOf type + sizeOf synthPendingDepth
-- Mathlib.Order.Lattice
inf_left_right_swap : ∀ {α : Type u} [inst : SemilatticeInf α] (a b c : α), a ⊓ b ⊓ c = c ⊓ b ⊓ a
-- Mathlib.Data.Setoid.Basic
Quotient.liftOn'.congr_simp : ∀ {α : Sort u_1} {φ : Sort u_4} {s₁ : Setoid α} (q q_1 : Quotient s₁),
  q = q_1 → ∀ (f f_1 : α → φ) (e_f : f = f_1) (h : ∀ (a b : α), s₁ a b → f a = f b), q.liftOn' f h = q_1.liftOn' f_1 ⋯